# HG changeset patch
# User haftmann
# Date 1278073398 -7200
# Node ID 71e84a203c1967050def2c2d3006c9764d68172b
# Parent  19e8b730ddeb0a823c36a62f1f09d23adad31f11
introduced distinct session HOL-Codegenerator_Test

diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/Codegenerator_Test/Candidates.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,25 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A huge collection of equations to generate code from *}
+
+theory Candidates
+imports
+  Complex_Main
+  Library
+  List_Prefix
+  "~~/src/HOL/Number_Theory/Primes"
+  "~~/src/HOL/ex/Records"
+begin
+
+inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+    empty: "sublist [] xs"
+  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
+  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
+
+code_pred sublist .
+
+(*avoid popular infix*)
+code_reserved SML upto
+
+end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/Codegenerator_Test/Candidates_Pretty.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,10 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Generating code using pretty literals and natural number literals  *}
+
+theory Candidates_Pretty
+imports Candidates Code_Char Efficient_Nat
+begin
+
+end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/Codegenerator_Test/Generate.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,15 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate
+imports Candidates
+begin
+
+export_code * in SML module_name Code_Test
+  in OCaml module_name Code_Test file -
+  in Haskell file -
+  in Scala file -
+
+end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Jul 02 14:23:18 2010 +0200
@@ -0,0 +1,20 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator using pretty literals *}
+
+theory Generate_Pretty
+imports Candidates_Pretty
+begin
+
+lemma [code, code del]: "nat_of_char = nat_of_char" ..
+lemma [code, code del]: "char_of_nat = char_of_nat" ..
+lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
+lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
+
+export_code * in SML module_name Code_Test
+  in OCaml module_name Code_Test file -
+  in Haskell file -
+  in Scala file -
+
+end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A huge collection of equations to generate code from *}
-
-theory Codegenerator_Candidates
-imports
-  Complex_Main
-  AssocList
-  Binomial
-  "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
-  Dlist
-  Fset
-  Enum
-  List_Prefix
-  More_List
-  Nat_Infinity
-  Nested_Environment
-  Option_ord
-  Permutation
-  "~~/src/HOL/Number_Theory/Primes"
-  Product_ord
-  "~~/src/HOL/ex/Records"
-  RBT
-  SetsAndFunctions
-  While_Combinator
-begin
-
-inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
-    empty: "sublist [] xs"
-  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
-  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
-
-code_pred sublist .
-
-(*avoid popular infix*)
-code_reserved SML upto
-
-end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/ex/Codegenerator_Pretty.thy
--- a/src/HOL/ex/Codegenerator_Pretty.thy	Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Generating code using pretty literals and natural number literals  *}
-
-theory Codegenerator_Pretty
-imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
-begin
-
-declare isnorm.simps [code del]
-
-end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/ex/Codegenerator_Pretty_Test.thy
--- a/src/HOL/ex/Codegenerator_Pretty_Test.thy	Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Pervasive test of code generator using pretty literals *}
-
-theory Codegenerator_Pretty_Test
-imports Codegenerator_Pretty
-begin
-
-export_code * in SML module_name CodegenTest
-  in OCaml module_name CodegenTest file -
-  in Haskell file -
-  in Scala file -
-
-end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/ex/Codegenerator_Test.thy
--- a/src/HOL/ex/Codegenerator_Test.thy	Fri Jul 02 14:23:17 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Pervasive test of code generator *}
-
-theory Codegenerator_Test
-imports Codegenerator_Candidates
-begin
-
-export_code * in SML module_name CodegenTest
-  in OCaml module_name CodegenTest file -
-  in Haskell file -
-  in Scala file -
-
-end
diff -r 19e8b730ddeb -r 71e84a203c19 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jul 02 14:23:17 2010 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Jul 02 14:23:18 2010 +0200
@@ -8,8 +8,6 @@
   "Efficient_Nat_examples",
   "FuncSet",
   "Eval_Examples",
-  "Codegenerator_Test",
-  "Codegenerator_Pretty_Test",
   "NormalForm"
 ];