Re: [isabelle] Get an ML value from a theory context

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
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
(which lives in the context of
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 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.

If you work properly on the Isabelle/ML level, within the HOL image, the datatype package is loaded and set up.
Hence, you can then access the structure simply by its name "Datatype_Data".


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