*To*: "Viorel Preoteasa" <viorel.preoteasa at aalto.fi>*Subject*: Re: [isabelle] Obtaining a list of theorems in ML*From*: "Lars Hupel" <hupel at in.tum.de>*Date*: Tue, 1 Sep 2015 16:30:30 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*Importance*: Normal*In-reply-to*: <55E5B0CC.7060803@aalto.fi>*References*: <55E4A2B5.1080300@wanadoo.fr> <55E5B0CC.7060803@aalto.fi>*Reply-to*: hupel at in.tum.de*User-agent*: Host Europe Webmailer/1.0

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

**Follow-Ups**:**Re: [isabelle] Obtaining a list of theorems in ML***From:*Viorel Preoteasa

**References**:**[isabelle] Obtaining a list of theorems in ML***From:*Viorel Preoteasa

- Previous by Date: [isabelle] Obtaining a list of theorems in ML
- Next by Date: Re: [isabelle] Obtaining a list of theorems in ML
- Previous by Thread: [isabelle] Obtaining a list of theorems in ML
- Next by Thread: Re: [isabelle] Obtaining a list of theorems in ML
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list