Moved code generator setup from Recdef to Inductive.
--- a/src/HOL/Inductive.thy Mon Dec 10 15:16:49 2001 +0100
+++ b/src/HOL/Inductive.thy Mon Dec 10 15:17:49 2001 +0100
@@ -9,11 +9,14 @@
theory Inductive = Gfp + Sum_Type + Relation
files
("Tools/inductive_package.ML")
+ ("Tools/inductive_codegen.ML")
("Tools/datatype_aux.ML")
("Tools/datatype_prop.ML")
("Tools/datatype_rep_proofs.ML")
("Tools/datatype_abs_proofs.ML")
("Tools/datatype_package.ML")
+ ("Tools/datatype_codegen.ML")
+ ("Tools/recfun_codegen.ML")
("Tools/primrec_package.ML"):
@@ -69,6 +72,9 @@
text {* Package setup. *}
+use "Tools/recfun_codegen.ML"
+setup RecfunCodegen.setup
+
use "Tools/datatype_aux.ML"
use "Tools/datatype_prop.ML"
use "Tools/datatype_rep_proofs.ML"
@@ -76,7 +82,12 @@
use "Tools/datatype_package.ML"
setup DatatypePackage.setup
+use "Tools/datatype_codegen.ML"
+setup DatatypeCodegen.setup
+
+use "Tools/inductive_codegen.ML"
+setup InductiveCodegen.setup
+
use "Tools/primrec_package.ML"
-setup PrimrecPackage.setup
end
--- a/src/HOL/Recdef.thy Mon Dec 10 15:16:49 2001 +0100
+++ b/src/HOL/Recdef.thy Mon Dec 10 15:17:49 2001 +0100
@@ -15,9 +15,7 @@
("../TFL/thry.ML")
("../TFL/tfl.ML")
("../TFL/post.ML")
- ("Tools/recdef_package.ML")
- ("Tools/basic_codegen.ML")
- ("Tools/inductive_codegen.ML"):
+ ("Tools/recdef_package.ML"):
lemma tfl_eq_True: "(x = True) --> x"
by blast
@@ -52,11 +50,7 @@
use "../TFL/tfl.ML"
use "../TFL/post.ML"
use "Tools/recdef_package.ML"
-use "Tools/basic_codegen.ML"
-use "Tools/inductive_codegen.ML"
setup RecdefPackage.setup
-setup BasicCodegen.setup
-setup InductiveCodegen.setup
lemmas [recdef_simp] =
inv_image_def