*To*: <hupel at in.tum.de>*Subject*: Re: [isabelle] Obtaining a list of theorems in ML*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Tue, 1 Sep 2015 19:31:38 +0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5d46df3a71430e0b047b6e12498ec4b8-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WEJQS1kPV0F3BFFLXFlYLkQGW1tYQV9dWwg=-webmailer1@server02.webmailer.hosteurope.de>*References*: <55E4A2B5.1080300@wanadoo.fr> <55E5B0CC.7060803@aalto.fi> <5d46df3a71430e0b047b6e12498ec4b8-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WEJQS1kPV0F3BFFLXFlYLkQGW1tYQV9dWwg=-webmailer1@server02.webmailer.hosteurope.de>*User-agent*: Mozilla/5.0 (Windows NT 6.3; WOW64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

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.

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, Viorel

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

**Re: [isabelle] Obtaining a list of theorems in ML***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Obtaining a list of theorems in ML
- Next by Date: Re: [isabelle] Obtaining a list of theorems in ML
- Previous by Thread: Re: [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