[isabelle] Get an ML value from a theory context



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 the
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.

 Jonathan
 




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