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

Hi Lars,

Thank you for your message.

On 9/1/2015 5:30 PM, Lars Hupel wrote:
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"

This seems to give me what I need.
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.
The first thing I run into was Attribthms , but I did not manage to use it.

These theorems are all fixed under some declaration:

theorems MySimps = ...

and in different theories I need to use different theorems, so I will just
define MySimps to be one or another list.

Best regards,


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