--- a/NEWS Tue Oct 31 09:29:18 2006 +0100
+++ b/NEWS Tue Oct 31 14:58:12 2006 +0100
@@ -52,7 +52,7 @@
code for ML and Haskell (including "class"es). A short usage sketch:
internal compilation:
- code_gen <list of constants (term syntax)> (SML -)
+ code_gen <list of constants (term syntax)> (SML *)
writing SML code to a file:
code_gen <list of constants (term syntax)> (SML <filename>)
writing Haskell code to a bunch of files:
--- a/src/HOL/Extraction/QuotRem.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Extraction/QuotRem.thy Tue Oct 31 14:58:12 2006 +0100
@@ -49,6 +49,6 @@
contains
test = "division 9 2"
-code_gen division (SML -)
+code_gen division (SML *)
end
--- a/src/HOL/Lambda/WeakNorm.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Tue Oct 31 14:58:12 2006 +0100
@@ -584,7 +584,7 @@
*}
code_gen
- type_NF (SML -) (SML _)
+ type_NF (SML *)
ML {*
structure Norm = ROOT.WeakNorm;
--- a/src/HOL/Library/EfficientNat.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Tue Oct 31 14:58:12 2006 +0100
@@ -133,8 +133,8 @@
(Haskell "0")
code_const "Suc"
- (SML "IntInf.+ (__, 1)")
- (Haskell "!(__ + 1)")
+ (SML "IntInf.+ ((_), 1)")
+ (Haskell "!((_) + 1)")
setup {*
CodegenData.del_datatype "nat"
--- a/src/HOL/Library/ExecutableRat.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy Tue Oct 31 14:58:12 2006 +0100
@@ -143,7 +143,7 @@
"inverse \<Colon> rat \<Rightarrow> rat"
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
"Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
- (SML -)
+ (SML *)
section {* type serializations *}
--- a/src/HOL/Library/ExecutableSet.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Tue Oct 31 14:58:12 2006 +0100
@@ -285,7 +285,7 @@
Bex \<equiv> Blex
code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
- image Union Inter UNION INTER Ball Bex (SML -)
+ image Union Inter UNION INTER Ball Bex (SML *)
subsection {* type serializations *}
--- a/src/HOL/ex/Classpackage.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/Classpackage.thy Tue Oct 31 14:58:12 2006 +0100
@@ -323,7 +323,7 @@
code_gen X Y (SML) (Haskell)
code_gen x1 x2 y2 (SML) (Haskell)
-code_gen (SML -)
+code_gen (SML *)
code_gen (Haskell -)
end
--- a/src/HOL/ex/CodeCollections.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy Tue Oct 31 14:58:12 2006 +0100
@@ -406,7 +406,7 @@
code_gen test1
code_gen test2
-code_gen (SML -)
+code_gen (SML *)
code_gen (Haskell -)
end
\ No newline at end of file
--- a/src/HOL/ex/CodeRandom.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy Tue Oct 31 14:58:12 2006 +0100
@@ -182,6 +182,6 @@
(SML "case _ (Random.seed ()) of (x, '_) => x")
code_gen select select_weight
- (SML -)
+ (SML *)
end
\ No newline at end of file
--- a/src/HOL/ex/Codegenerator.thy Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy Tue Oct 31 14:58:12 2006 +0100
@@ -5,7 +5,7 @@
header {* Test and Examples for code generator *}
theory Codegenerator
-imports Main Records
+imports Main (*"~/projects/codegen/thy/CodegenSetup"*) Records
begin
subsection {* booleans *}
@@ -197,7 +197,7 @@
"Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
"Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
-code_gen (SML -)
+code_gen (SML *)
code_gen (Haskell -)
end
\ No newline at end of file