Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed code generator theorem generation
authorhaftmann
Tue, 08 Aug 2006 08:20:24 +0200
changeset 20357 5fb92bd3aaea
parent 20356 21e7e9093940
child 20358 ccad73da6f61
fixed code generator theorem generation
src/HOL/Tools/typedef_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/typedef_package.ML	Tue Aug 08 08:19:47 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Aug 08 08:20:24 2006 +0200
@@ -24,6 +24,7 @@
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
   val setup: theory -> theory
+  structure TypedefData: THEORY_DATA
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
isabelle