Re: [isabelle] named theorems in Isabelle/ML

On Sat, 6 Dec 2014, Christian Sternagel wrote:

Named_Theorems.get ctxt @{named_theorems "a"}

(I couldn't find documentation for this antiquotation though.)

As usual the default documentation is two-fold:

  (1) The definition in ML, which is accessible by C-hover click on the
      antiquotation name.

  (2) Example applications that are lying around in the Isabelle sources,
      which can be found by a hyper-search of "@{named_theorems".

The implementation idiom to have an abstract formal concept like "named_theorems" with a command to define it and an antiquotation to refer to it in the ML sources is similar to 'simproc_setup' and @{simproc}.

The formal antiquotation also has the advantage to participate in completion, without further ado.

BTW, this updated version of named_theorems actually belongs to the ongoing development after Isabelle2014, i.e. is not present in the official release. At the moment we are talking about something like Isabelle/364992cd3c50.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.