Re: [isabelle] Obtaining a list of theorems in ML



Hello Viorel,

> So I need a function "GetMyThms ctxt" which does exactly the same
> as @{thms MyTh}, but for ctxt parameter, and not the current context.

this can be achieved like so:

  Proof_Context.get_thms ctxt "append.simps"

Depending on where you get these theorem names from, it might make more
sense to use the appropriate parsers which produce theorems directly (e.g.
Attrib.thms). I would strongly encourage to use those instead.

Cheers
Lars




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