# HG changeset patch
# User berghofe
# Date 999268106 -7200
# Node ID 0c0d2332e8f0fc868ce63e5c7771a4f3a3eceebb
# Parent  da74db1373eab2f027f01970b73debfae8105614
Added code generator setup.

diff -r da74db1373ea -r 0c0d2332e8f0 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Aug 31 16:27:43 2001 +0200
+++ b/src/HOL/Main.thy	Fri Aug 31 16:28:26 2001 +0200
@@ -15,4 +15,28 @@
 lemmas rev_induct [case_names Nil snoc] = rev_induct
   and rev_cases [case_names Nil snoc] = rev_exhaust
 
+(** configuration of code generator **)
+
+types_code
+  "bool"  ("bool")
+  "*"     ("prod")
+  "list"  ("list")
+
+consts_code
+  "op ="    ("(_ =/ _)")
+
+  "True"    ("true")
+  "False"   ("false")
+  "Not"     ("not")
+  "op |"    ("(_ orelse/ _)")
+  "op &"    ("(_ andalso/ _)")
+  "If"      ("(if _/ then _/ else _)")
+
+  "Pair"    ("(_,/ _)")
+  "fst"     ("fst")
+  "snd"     ("snd")
+
+  "Nil"     ("[]")
+  "Cons"    ("(_ ::/ _)")
+  
 end
diff -r da74db1373ea -r 0c0d2332e8f0 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Fri Aug 31 16:27:43 2001 +0200
+++ b/src/HOL/Recdef.thy	Fri Aug 31 16:28:26 2001 +0200
@@ -15,7 +15,9 @@
   ("../TFL/thry.ML")
   ("../TFL/tfl.ML")
   ("../TFL/post.ML")
-  ("Tools/recdef_package.ML"):
+  ("Tools/recdef_package.ML")
+  ("Tools/basic_codegen.ML")
+  ("Tools/inductive_codegen.ML"):
 
 lemma tfl_eq_True: "(x = True) --> x"
   by blast
@@ -50,7 +52,11 @@
 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