renamed keyword "to" to "module_name"
authorhaftmann
Mon Aug 13 21:22:37 2007 +0200 (2007-08-13)
changeset 242491f60b45c5f97
parent 24248 d276e4b53d6b
child 24250 c59c09b09794
renamed keyword "to" to "module_name"
etc/isar-keywords-HOL-Nominal.el
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Codegenerator_Pretty.thy
src/HOL/ex/Reflected_Presburger.thy
     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"