1.1 --- a/etc/isar-keywords-HOL-Nominal.el Mon Aug 13 21:22:36 2007 +0200
1.2 +++ b/etc/isar-keywords-HOL-Nominal.el Mon Aug 13 21:22:37 2007 +0200
1.3 @@ -221,7 +221,6 @@
1.4 "undo"
1.5 "undos_proof"
1.6 "unfolding"
1.7 - "update_thy"
1.8 "use"
1.9 "use_thy"
1.10 "using"
1.11 @@ -262,6 +261,7 @@
1.12 "inject"
1.13 "invariant"
1.14 "is"
1.15 + "module_name"
1.16 "monos"
1.17 "morphisms"
1.18 "notes"
1.19 @@ -274,7 +274,6 @@
1.20 "sequential"
1.21 "shows"
1.22 "structure"
1.23 - "to"
1.24 "unchecked"
1.25 "uses"
1.26 "where"))
1.27 @@ -356,7 +355,6 @@
1.28 "touch_child_thys"
1.29 "touch_thy"
1.30 "typ"
1.31 - "update_thy"
1.32 "use"
1.33 "use_thy"
1.34 "value"
2.1 --- a/etc/isar-keywords-ZF.el Mon Aug 13 21:22:36 2007 +0200
2.2 +++ b/etc/isar-keywords-ZF.el Mon Aug 13 21:22:37 2007 +0200
2.3 @@ -110,7 +110,6 @@
2.4 "no_syntax"
2.5 "no_translations"
2.6 "nonterminals"
2.7 - "normal_form"
2.8 "notation"
2.9 "note"
2.10 "obtain"
2.11 @@ -202,7 +201,6 @@
2.12 "undo"
2.13 "undos_proof"
2.14 "unfolding"
2.15 - "update_thy"
2.16 "use"
2.17 "use_thy"
2.18 "using"
2.19 @@ -241,6 +239,7 @@
2.20 "infixr"
2.21 "intros"
2.22 "is"
2.23 + "module_name"
2.24 "monos"
2.25 "notes"
2.26 "obtains"
2.27 @@ -250,7 +249,6 @@
2.28 "recursor_eqns"
2.29 "shows"
2.30 "structure"
2.31 - "to"
2.32 "type_elims"
2.33 "type_intros"
2.34 "unchecked"
2.35 @@ -290,7 +288,6 @@
2.36 "header"
2.37 "help"
2.38 "kill_thy"
2.39 - "normal_form"
2.40 "pr"
2.41 "pretty_setmargin"
2.42 "prf"
2.43 @@ -332,7 +329,6 @@
2.44 "touch_child_thys"
2.45 "touch_thy"
2.46 "typ"
2.47 - "update_thy"
2.48 "use"
2.49 "use_thy"
2.50 "value"
3.1 --- a/etc/isar-keywords.el Mon Aug 13 21:22:36 2007 +0200
3.2 +++ b/etc/isar-keywords.el Mon Aug 13 21:22:37 2007 +0200
3.3 @@ -222,7 +222,6 @@
3.4 "undo"
3.5 "undos_proof"
3.6 "unfolding"
3.7 - "update_thy"
3.8 "use"
3.9 "use_thy"
3.10 "using"
3.11 @@ -267,6 +266,7 @@
3.12 "internals"
3.13 "is"
3.14 "lazy"
3.15 + "module_name"
3.16 "monos"
3.17 "morphisms"
3.18 "notes"
3.19 @@ -370,7 +370,6 @@
3.20 "touch_child_thys"
3.21 "touch_thy"
3.22 "typ"
3.23 - "update_thy"
3.24 "use"
3.25 "use_thy"
3.26 "value"
4.1 --- a/src/HOL/Complex/ex/MIR.thy Mon Aug 13 21:22:36 2007 +0200
4.2 +++ b/src/HOL/Complex/ex/MIR.thy Mon Aug 13 21:22:37 2007 +0200
4.3 @@ -5778,9 +5778,10 @@
4.4 "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
4.5
4.6 code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
4.7 - in SML to Mir
4.8 -
4.9 -code_gen mircfrqe mirlfrqe in SML to Mir file "raw_mir.ML"
4.10 + in SML module_name Mir
4.11 +
4.12 +(*code_gen mircfrqe mirlfrqe
4.13 + in SML module_name Mir file "raw_mir.ML"*)
4.14
4.15 ML "set Toplevel.timing"
4.16 ML "Mir.test1 ()"
5.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Aug 13 21:22:36 2007 +0200
5.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Aug 13 21:22:37 2007 +0200
5.3 @@ -1993,7 +1993,7 @@
5.4 "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
5.5 (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
5.6
5.7 -code_gen linrqe ferrack_test in SML to Ferrack
5.8 +code_gen linrqe ferrack_test in SML module_name Ferrack
5.9
5.10 (*code_module Ferrack
5.11 contains
6.1 --- a/src/HOL/Extraction/Higman.thy Mon Aug 13 21:22:36 2007 +0200
6.2 +++ b/src/HOL/Extraction/Higman.thy Mon Aug 13 21:22:37 2007 +0200
6.3 @@ -427,7 +427,7 @@
6.4 code_datatype L0 L1 arbitrary_LT
6.5 code_datatype T0 T1 T2 arbitrary_TT
6.6
6.7 -code_gen higman_idx in SML to Higman
6.8 +code_gen higman_idx in SML module_name Higman
6.9
6.10 ML {*
6.11 local
7.1 --- a/src/HOL/Extraction/Pigeonhole.thy Mon Aug 13 21:22:36 2007 +0200
7.2 +++ b/src/HOL/Extraction/Pigeonhole.thy Mon Aug 13 21:22:37 2007 +0200
7.3 @@ -303,36 +303,36 @@
7.4 (* this is justified since for valid inputs this "arbitrary" will be dropped
7.5 in the next recursion step in pigeonhole_def *)
7.6
7.7 -code_module PH
7.8 +code_module PH1
7.9 contains
7.10 test = test
7.11 test' = test'
7.12 test'' = test''
7.13
7.14 -code_gen test test' test'' in SML to PH2
7.15 +code_gen test test' test'' in SML module_name PH2
7.16
7.17 -ML "timeit (PH.test 10)"
7.18 +ML "timeit (PH1.test 10)"
7.19 ML "timeit (PH2.test 10)"
7.20
7.21 -ML "timeit (PH.test' 10)"
7.22 +ML "timeit (PH1.test' 10)"
7.23 ML "timeit (PH2.test' 10)"
7.24
7.25 -ML "timeit (PH.test 20)"
7.26 +ML "timeit (PH1.test 20)"
7.27 ML "timeit (PH2.test 20)"
7.28
7.29 -ML "timeit (PH.test' 20)"
7.30 +ML "timeit (PH1.test' 20)"
7.31 ML "timeit (PH2.test' 20)"
7.32
7.33 -ML "timeit (PH.test 25)"
7.34 +ML "timeit (PH1.test 25)"
7.35 ML "timeit (PH2.test 25)"
7.36
7.37 -ML "timeit (PH.test' 25)"
7.38 +ML "timeit (PH1.test' 25)"
7.39 ML "timeit (PH2.test' 25)"
7.40
7.41 -ML "timeit (PH.test 500)"
7.42 +ML "timeit (PH1.test 500)"
7.43 ML "timeit (PH2.test 500)"
7.44
7.45 -ML "timeit PH.test''"
7.46 +ML "timeit PH1.test''"
7.47 ML "timeit PH2.test''"
7.48
7.49 end
8.1 --- a/src/HOL/Lambda/WeakNorm.thy Mon Aug 13 21:22:36 2007 +0200
8.2 +++ b/src/HOL/Lambda/WeakNorm.thy Mon Aug 13 21:22:37 2007 +0200
8.3 @@ -581,7 +581,7 @@
8.4 int :: "nat \<Rightarrow> int" where
8.5 "int \<equiv> of_nat"
8.6
8.7 -code_gen type_NF nat int in SML to Norm
8.8 +code_gen type_NF nat int in SML module_name Norm
8.9
8.10 ML {*
8.11 val nat_of_int = Norm.nat o IntInf.fromInt;
9.1 --- a/src/HOL/ex/Classpackage.thy Mon Aug 13 21:22:36 2007 +0200
9.2 +++ b/src/HOL/ex/Classpackage.thy Mon Aug 13 21:22:37 2007 +0200
9.3 @@ -328,7 +328,7 @@
9.4 definition "x2 = X (1::int) 2 3"
9.5 definition "y2 = Y (1::int) 2 3"
9.6
9.7 -code_gen x1 x2 y2 in SML to Classpackage
9.8 +code_gen x1 x2 y2 in SML module_name Classpackage
9.9 in OCaml file -
9.10 in Haskell file -
9.11
10.1 --- a/src/HOL/ex/Codegenerator.thy Mon Aug 13 21:22:36 2007 +0200
10.2 +++ b/src/HOL/ex/Codegenerator.thy Mon Aug 13 21:22:37 2007 +0200
10.3 @@ -8,7 +8,7 @@
10.4 imports ExecutableContent
10.5 begin
10.6
10.7 -code_gen "*" in SML to CodegenTest
10.8 +code_gen "*" in SML module_name CodegenTest
10.9 in OCaml file -
10.10 in Haskell file -
10.11
11.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy Mon Aug 13 21:22:36 2007 +0200
11.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Mon Aug 13 21:22:37 2007 +0200
11.3 @@ -49,7 +49,7 @@
11.4 definition
11.5 "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
11.6
11.7 -code_gen foobar foobar' in SML to Foo
11.8 +code_gen foobar foobar' in SML module_name Foo
11.9 in OCaml file -
11.10 in Haskell file -
11.11 ML {* (Foo.foobar, Foo.foobar') *}
12.1 --- a/src/HOL/ex/Reflected_Presburger.thy Mon Aug 13 21:22:36 2007 +0200
12.2 +++ b/src/HOL/ex/Reflected_Presburger.thy Mon Aug 13 21:22:37 2007 +0200
12.3 @@ -1936,8 +1936,8 @@
12.4 (Bound 2))))))))"
12.5
12.6 code_reserved SML oo
12.7 -code_gen pa cooper_test in SML to GeneratedCooper
12.8 -(*code_gen pa in SML to GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
12.9 +code_gen pa cooper_test in SML module_name GeneratedCooper
12.10 +(*code_gen pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
12.11
12.12 ML {* GeneratedCooper.cooper_test () *}
12.13 use "coopereif.ML"