*To*: Jonathan von Schroeder <jonathan.von_schroeder at dfki.de>*Subject*: Re: [isabelle] Get an ML value from a theory context*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Thu, 04 Aug 2011 13:50:12 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1761421701.4856.1312369046188.JavaMail.open-xchange@ox6>*References*: <1761421701.4856.1312369046188.JavaMail.open-xchange@ox6>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.18) Gecko/20110617 Thunderbird/3.1.11

On 08/03/2011 12:57 PM, Jonathan von Schroeder wrote:

Hello all, I'm currently working on a way to export Isabelle/HOL type definitions and their attached (user defined) axioms/theorems from a given theory in Isabelle. I have already managed to get this workign by simply going through all the constants, axioms and theorems present in the theories' context. But unluckily I currently get more axioms / theorems than I'm interested in, because thep, theorems automatically generated by http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/ are not really "user generated" and thus do not foll within the scope of theorems I wish to export. Thus I'd really like to have (in the top-level raw ML loop) access to the structure http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Tools/Datatype/datatype_data.ML (which lives in the context of http://isabelle.in.tum.de/repos/isabelle/file/6d736d983d5c/src/HOL/Datatype.thy from what i can tell) to be able to figure out which theorems were generated by the Datatype-Tool. Does anybody have any suggestions on how to do this, because the Manual http://isabelle.in.tum.de/doc/implementation.pdf only mentions on page 11 that "... [the function factorial] is not yet accessible in the preceding paragraph, nor in a different theory that is independent from the current one in the import hierarchy", but I wasn't able to find any information on how to "get" access to it (or for that matter to any ml functions / structures defined within a theory). I'd greatly appreciate any information anybody can provide on this matter.

Hence, you can then access the structure simply by its name "Datatype_Data". Lukas

Jonathan

**Follow-Ups**:**Re: [isabelle] Get an ML value from a theory context***From:*Jonathan von Schroeder

**References**:**[isabelle] Get an ML value from a theory context***From:*Jonathan von Schroeder

- Previous by Date: [isabelle] VSTTE 2012 : Fourth Call for Papers - 4 weeks to go
- Next by Date: [isabelle] A special notation for function application
- Previous by Thread: [isabelle] Get an ML value from a theory context
- Next by Thread: Re: [isabelle] Get an ML value from a theory context
- Cl-isabelle-users August 2011 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