[isabelle] named theorems in Isabelle/ML



Dear all,

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"

This works, but it feels strange to add this Theory name prefix (although it would not be strictly necessary, I like to avoid potential clashes).

Moreover, how do I add new theorems to an existing bundle? I.e., the equivalent of

  declare some_thm [a]

in Isabelle/ML?

cheers

chris




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