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.)

cheers

chris

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):

   Ac_Simps.get
   Ac_Simps.add_thm
   Ac_Simps.del_thm

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

   -- Lars





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