--- a/NEWS Mon Nov 27 12:12:18 2006 +0100
+++ b/NEWS Mon Nov 27 13:42:30 2006 +0100
@@ -63,7 +63,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/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon Nov 27 13:42:30 2006 +0100
@@ -153,7 +153,7 @@
This executable specification is now turned to SML code:
*}
-code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac.ML")
+code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML")
text {*
The @{text "\<CODEGEN>"} command takes a space-separated list of
@@ -269,7 +269,7 @@
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
by simp
-code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick1.ML")
+code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
text {*
This theorem is now added to the function equation table:
@@ -282,7 +282,7 @@
lemmas [code nofunc] = pick.simps
-code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick2.ML")
+code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML")
text {*
\lstsml{Thy/examples/pick2.ML}
@@ -298,7 +298,7 @@
"fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
by (cases n) simp_all
-code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac_case.ML")
+code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML")
text {*
\lstsml{Thy/examples/fac_case.ML}
@@ -377,7 +377,7 @@
The whole code in SML with explicit dictionary passing:
*}
-code_gen dummy (*<*)(SML *)(*>*)(SML "examples/class.ML")
+code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML")
text {*
\lstsml{Thy/examples/class.ML}
@@ -557,7 +557,7 @@
(SML and and and)
(*>*)
-code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_literal.ML")
+code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML")
text {*
\lstsml{Thy/examples/bool_literal.ML}
@@ -600,7 +600,7 @@
After this setup, code looks quite more readable:
*}
-code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_mlbool.ML")
+code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML")
text {*
\lstsml{Thy/examples/bool_mlbool.ML}
@@ -616,7 +616,7 @@
code_const %tt "op \<and>"
(SML infixl 1 "andalso")
-code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_infix.ML")
+code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML")
text {*
\lstsml{Thy/examples/bool_infix.ML}
@@ -675,7 +675,7 @@
and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
-code_gen double_inc (*<*)(SML *)(*>*)(SML "examples/integers.ML")
+code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML")
text {*
resulting in:
@@ -727,7 +727,7 @@
performs an explicit equality check.
*}
-code_gen collect_duplicates (*<*)(SML *)(*>*)(SML "examples/collect_duplicates.ML")
+code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
text {*
\lstsml{Thy/examples/collect_duplicates.ML}
@@ -803,7 +803,7 @@
Then everything goes fine:
*}
-code_gen lookup (*<*)(SML *)(*>*)(SML "examples/lookup.ML")
+code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML")
text {*
\lstsml{Thy/examples/lookup.ML}
@@ -856,7 +856,7 @@
*}
code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
- (*<*)(SML *)(*>*)(SML "examples/lexicographic.ML")
+ (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
text {*
\lstsml{Thy/examples/lexicographic.ML}
@@ -960,7 +960,7 @@
lemma [code func]:
"insert = insert" ..
-code_gen dummy_set foobar_set (*<*)(SML *)(*>*)(SML "examples/dirty_set.ML")
+code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML")
text {*
\lstsml{Thy/examples/dirty_set.ML}
@@ -1087,7 +1087,7 @@
declare dummy_option.simps [code func]
(*>*)
-code_gen dummy_option (*<*)(SML *)(*>*)(SML "examples/arbitrary.ML")
+code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
text {*
\lstsml{Thy/examples/arbitrary.ML}
--- a/src/HOL/Extraction/Higman.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/Higman.thy Mon Nov 27 13:42:30 2006 +0100
@@ -337,7 +337,7 @@
end;
*}
-code_gen good_prefix (SML *)
+code_gen good_prefix (SML #)
ML {*
local
--- a/src/HOL/Extraction/Pigeonhole.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy Mon Nov 27 13:42:30 2006 +0100
@@ -316,7 +316,7 @@
definition
"test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
-code_gen test test' "op !" (SML *)
+code_gen test test' "op !" (SML #)
ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
--- a/src/HOL/Extraction/QuotRem.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/QuotRem.thy Mon Nov 27 13:42:30 2006 +0100
@@ -49,6 +49,6 @@
contains
test = "division 9 2"
-code_gen division (SML *)
+code_gen division (SML #)
end
--- a/src/HOL/Library/ExecutableRat.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy Mon Nov 27 13:42:30 2006 +0100
@@ -137,7 +137,7 @@
"inverse \<Colon> rat \<Rightarrow> rat"
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
"op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
- (SML *)
+ (SML #)
section {* type serializations *}
--- a/src/HOL/ex/Classpackage.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/Classpackage.thy Mon Nov 27 13:42:30 2006 +0100
@@ -320,7 +320,7 @@
definition "y2 = Y (1::int) 2 3"
code_gen "op \<otimes>" \<one> inv
-code_gen X Y (SML *) (Haskell -)
-code_gen x1 x2 y2 (SML *) (Haskell -)
+code_gen X Y (SML #) (Haskell -)
+code_gen x1 x2 y2 (SML #) (Haskell -)
end
--- a/src/HOL/ex/CodeCollections.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy Mon Nov 27 13:42:30 2006 +0100
@@ -198,7 +198,7 @@
code_gen test3
-code_gen (SML *)
+code_gen (SML #)
code_gen (Haskell -)
end
\ No newline at end of file
--- a/src/HOL/ex/CodeRandom.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy Mon Nov 27 13:42:30 2006 +0100
@@ -187,7 +187,7 @@
(SML "case _ (Random.seed ()) of (x, '_) => x")
code_gen select select_weight
- (SML *)
+ (SML #)
code_gen (SML -)
--- a/src/HOL/ex/Codegenerator.thy Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy Mon Nov 27 13:42:30 2006 +0100
@@ -188,6 +188,6 @@
"op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
"op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
-code_gen (SML *) (Haskell -)
+code_gen (SML #) (Haskell -)
end
\ No newline at end of file