--- a/etc/isar-keywords-HOL-Nominal.el Mon Aug 13 21:22:36 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el Mon Aug 13 21:22:37 2007 +0200
@@ -221,7 +221,6 @@
"undo"
"undos_proof"
"unfolding"
- "update_thy"
"use"
"use_thy"
"using"
@@ -262,6 +261,7 @@
"inject"
"invariant"
"is"
+ "module_name"
"monos"
"morphisms"
"notes"
@@ -274,7 +274,6 @@
"sequential"
"shows"
"structure"
- "to"
"unchecked"
"uses"
"where"))
@@ -356,7 +355,6 @@
"touch_child_thys"
"touch_thy"
"typ"
- "update_thy"
"use"
"use_thy"
"value"
--- a/etc/isar-keywords-ZF.el Mon Aug 13 21:22:36 2007 +0200
+++ b/etc/isar-keywords-ZF.el Mon Aug 13 21:22:37 2007 +0200
@@ -110,7 +110,6 @@
"no_syntax"
"no_translations"
"nonterminals"
- "normal_form"
"notation"
"note"
"obtain"
@@ -202,7 +201,6 @@
"undo"
"undos_proof"
"unfolding"
- "update_thy"
"use"
"use_thy"
"using"
@@ -241,6 +239,7 @@
"infixr"
"intros"
"is"
+ "module_name"
"monos"
"notes"
"obtains"
@@ -250,7 +249,6 @@
"recursor_eqns"
"shows"
"structure"
- "to"
"type_elims"
"type_intros"
"unchecked"
@@ -290,7 +288,6 @@
"header"
"help"
"kill_thy"
- "normal_form"
"pr"
"pretty_setmargin"
"prf"
@@ -332,7 +329,6 @@
"touch_child_thys"
"touch_thy"
"typ"
- "update_thy"
"use"
"use_thy"
"value"
--- a/etc/isar-keywords.el Mon Aug 13 21:22:36 2007 +0200
+++ b/etc/isar-keywords.el Mon Aug 13 21:22:37 2007 +0200
@@ -222,7 +222,6 @@
"undo"
"undos_proof"
"unfolding"
- "update_thy"
"use"
"use_thy"
"using"
@@ -267,6 +266,7 @@
"internals"
"is"
"lazy"
+ "module_name"
"monos"
"morphisms"
"notes"
@@ -370,7 +370,6 @@
"touch_child_thys"
"touch_thy"
"typ"
- "update_thy"
"use"
"use_thy"
"value"
--- a/src/HOL/Complex/ex/MIR.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Mon Aug 13 21:22:37 2007 +0200
@@ -5778,9 +5778,10 @@
"test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
- in SML to Mir
-
-code_gen mircfrqe mirlfrqe in SML to Mir file "raw_mir.ML"
+ in SML module_name Mir
+
+(*code_gen mircfrqe mirlfrqe
+ in SML module_name Mir file "raw_mir.ML"*)
ML "set Toplevel.timing"
ML "Mir.test1 ()"
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Aug 13 21:22:37 2007 +0200
@@ -1993,7 +1993,7 @@
"ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
(E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
-code_gen linrqe ferrack_test in SML to Ferrack
+code_gen linrqe ferrack_test in SML module_name Ferrack
(*code_module Ferrack
contains
--- a/src/HOL/Extraction/Higman.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy Mon Aug 13 21:22:37 2007 +0200
@@ -427,7 +427,7 @@
code_datatype L0 L1 arbitrary_LT
code_datatype T0 T1 T2 arbitrary_TT
-code_gen higman_idx in SML to Higman
+code_gen higman_idx in SML module_name Higman
ML {*
local
--- a/src/HOL/Extraction/Pigeonhole.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Mon Aug 13 21:22:37 2007 +0200
@@ -303,36 +303,36 @@
(* this is justified since for valid inputs this "arbitrary" will be dropped
in the next recursion step in pigeonhole_def *)
-code_module PH
+code_module PH1
contains
test = test
test' = test'
test'' = test''
-code_gen test test' test'' in SML to PH2
+code_gen test test' test'' in SML module_name PH2
-ML "timeit (PH.test 10)"
+ML "timeit (PH1.test 10)"
ML "timeit (PH2.test 10)"
-ML "timeit (PH.test' 10)"
+ML "timeit (PH1.test' 10)"
ML "timeit (PH2.test' 10)"
-ML "timeit (PH.test 20)"
+ML "timeit (PH1.test 20)"
ML "timeit (PH2.test 20)"
-ML "timeit (PH.test' 20)"
+ML "timeit (PH1.test' 20)"
ML "timeit (PH2.test' 20)"
-ML "timeit (PH.test 25)"
+ML "timeit (PH1.test 25)"
ML "timeit (PH2.test 25)"
-ML "timeit (PH.test' 25)"
+ML "timeit (PH1.test' 25)"
ML "timeit (PH2.test' 25)"
-ML "timeit (PH.test 500)"
+ML "timeit (PH1.test 500)"
ML "timeit (PH2.test 500)"
-ML "timeit PH.test''"
+ML "timeit PH1.test''"
ML "timeit PH2.test''"
end
--- a/src/HOL/Lambda/WeakNorm.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Mon Aug 13 21:22:37 2007 +0200
@@ -581,7 +581,7 @@
int :: "nat \<Rightarrow> int" where
"int \<equiv> of_nat"
-code_gen type_NF nat int in SML to Norm
+code_gen type_NF nat int in SML module_name Norm
ML {*
val nat_of_int = Norm.nat o IntInf.fromInt;
--- a/src/HOL/ex/Classpackage.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy Mon Aug 13 21:22:37 2007 +0200
@@ -328,7 +328,7 @@
definition "x2 = X (1::int) 2 3"
definition "y2 = Y (1::int) 2 3"
-code_gen x1 x2 y2 in SML to Classpackage
+code_gen x1 x2 y2 in SML module_name Classpackage
in OCaml file -
in Haskell file -
--- a/src/HOL/ex/Codegenerator.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy Mon Aug 13 21:22:37 2007 +0200
@@ -8,7 +8,7 @@
imports ExecutableContent
begin
-code_gen "*" in SML to CodegenTest
+code_gen "*" in SML module_name CodegenTest
in OCaml file -
in Haskell file -
--- a/src/HOL/ex/Codegenerator_Pretty.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Mon Aug 13 21:22:37 2007 +0200
@@ -49,7 +49,7 @@
definition
"foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
-code_gen foobar foobar' in SML to Foo
+code_gen foobar foobar' in SML module_name Foo
in OCaml file -
in Haskell file -
ML {* (Foo.foobar, Foo.foobar') *}
--- a/src/HOL/ex/Reflected_Presburger.thy Mon Aug 13 21:22:36 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Mon Aug 13 21:22:37 2007 +0200
@@ -1936,8 +1936,8 @@
(Bound 2))))))))"
code_reserved SML oo
-code_gen pa cooper_test in SML to GeneratedCooper
-(*code_gen pa in SML to GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+code_gen pa cooper_test in SML module_name GeneratedCooper
+(*code_gen pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
ML {* GeneratedCooper.cooper_test () *}
use "coopereif.ML"