src/HOL/HOL.thy
changeset 9869 95dca9f991f2
parent 9852 6ca7fcac3e23
child 9890 144ecc001b8f
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 05 18:59:22 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 05 21:06:01 2000 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  *)
     1.5  
     1.6  theory HOL = CPure
     1.7 -files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") 
     1.8 -      ("Tools/meson.ML"):
     1.9 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    1.10 +  ("meson_lemmas.ML") ("Tools/meson.ML"):
    1.11  
    1.12  
    1.13  (** Core syntax **)
    1.14 @@ -54,7 +54,7 @@
    1.15  
    1.16  (* Overloaded Constants *)
    1.17  
    1.18 -axclass zero  < "term" 
    1.19 +axclass zero  < "term"
    1.20  axclass plus  < "term"
    1.21  axclass minus < "term"
    1.22  axclass times < "term"
    1.23 @@ -65,7 +65,7 @@
    1.24    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    1.25    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    1.26    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    1.27 -  abs		:: "('a::minus) => 'a"
    1.28 +  abs           :: "('a::minus) => 'a"
    1.29    *             :: "['a::times, 'a] => 'a"          (infixl 70)
    1.30    (*See Nat.thy for "^"*)
    1.31  
    1.32 @@ -193,7 +193,11 @@
    1.33  (* theory and package setup *)
    1.34  
    1.35  use "HOL_lemmas.ML"
    1.36 -use "cladata.ML"	setup hypsubst_setup setup Classical.setup setup clasetup
    1.37 +
    1.38 +use "cladata.ML"
    1.39 +setup hypsubst_setup
    1.40 +setup Classical.setup
    1.41 +setup clasetup
    1.42  
    1.43  lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
    1.44  proof (rule equal_intr_rule)
    1.45 @@ -216,12 +220,17 @@
    1.46  
    1.47  lemmas atomize = all_eq imp_eq
    1.48  
    1.49 -use "blastdata.ML"	setup Blast.setup
    1.50 -use "simpdata.ML"	setup Simplifier.setup
    1.51 -			setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    1.52 -                        setup Splitter.setup setup Clasimp.setup
    1.53 -			setup rulify_attrib_setup
    1.54 +use "blastdata.ML"
    1.55 +setup Blast.setup
    1.56  
    1.57 +use "simpdata.ML"
    1.58 +setup Simplifier.setup
    1.59 +setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    1.60 +setup Splitter.setup setup Clasimp.setup
    1.61 +setup rulify_attrib_setup
    1.62 +
    1.63 +use "meson_lemmas.ML"
    1.64  use "Tools/meson.ML"
    1.65 +setup meson_setup
    1.66  
    1.67  end