--- a/src/Tools/Code_Generator.thy Wed Sep 15 16:56:31 2010 +0200
+++ b/src/Tools/Code_Generator.thy Wed Sep 15 16:56:31 2010 +0200
@@ -21,10 +21,22 @@
"~~/src/Tools/Code/code_ml.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
- ("~~/src/Tools/Code/code_runtime.ML")
+ "~~/src/Tools/Code/code_runtime.ML"
"~~/src/Tools/nbe.ML"
begin
+setup {*
+ Auto_Solve.setup
+ #> Code_Preproc.setup
+ #> Code_Simp.setup
+ #> Code_ML.setup
+ #> Code_Haskell.setup
+ #> Code_Scala.setup
+ #> Code_Runtime.setup
+ #> Nbe.setup
+ #> Quickcheck.setup
+*}
+
code_datatype "TYPE('a\<Colon>{})"
definition holds :: "prop" where
@@ -52,20 +64,6 @@
by rule (rule holds)+
qed
-use "~~/src/Tools/Code/code_runtime.ML"
-
-setup {*
- Auto_Solve.setup
- #> Code_Preproc.setup
- #> Code_Simp.setup
- #> Code_ML.setup
- #> Code_Haskell.setup
- #> Code_Scala.setup
- #> Code_Runtime.setup
- #> Nbe.setup
- #> Quickcheck.setup
-*}
-
hide_const (open) holds
end