Re: [isabelle] named theorems in Isabelle/ML

Thanks Lars!

just for the record. Another way I spotted in the implementation manual is

Named_Theorems.get ctxt @{named_theorems "a"}

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



On 12/05/2014 11:51 PM, Lars Noschinski wrote:
On 05.12.2014 22:15, Christian Sternagel wrote:

how do I imitate addition and retrieval of named theorems in
Isabelle/ML. More specifically, to obtain all theorems in a named
theorem bundle "a" I currently do

   Proof_Context.get_thms ctxt "Theory_Name.a"

If you have access to the structure of the named theorems you can use
the functions of the Named_Thms functor. For example for the ac_simps
attribute (defined in ~~src/HOL/Groups.thy):


See also ~~/src/Pure/Tools/named_thms.ML

   -- Lars

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