diff -r 580c50fc6559 -r 95dca9f991f2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 05 18:59:22 2000 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 05 21:06:01 2000 +0200
@@ -7,8 +7,8 @@
 *)
 
 theory HOL = CPure
-files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") 
-      ("Tools/meson.ML"):
+files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+  ("meson_lemmas.ML") ("Tools/meson.ML"):
 
 
 (** Core syntax **)
@@ -54,7 +54,7 @@
 
 (* Overloaded Constants *)
 
-axclass zero  < "term" 
+axclass zero  < "term"
 axclass plus  < "term"
 axclass minus < "term"
 axclass times < "term"
@@ -65,7 +65,7 @@
   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
-  abs		:: "('a::minus) => 'a"
+  abs           :: "('a::minus) => 'a"
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
   (*See Nat.thy for "^"*)
 
@@ -193,7 +193,11 @@
 (* theory and package setup *)
 
 use "HOL_lemmas.ML"
-use "cladata.ML"	setup hypsubst_setup setup Classical.setup setup clasetup
+
+use "cladata.ML"
+setup hypsubst_setup
+setup Classical.setup
+setup clasetup
 
 lemma all_eq: "(!!x. P x) == Trueprop (ALL x. P x)"
 proof (rule equal_intr_rule)
@@ -216,12 +220,17 @@
 
 lemmas atomize = all_eq imp_eq
 
-use "blastdata.ML"	setup Blast.setup
-use "simpdata.ML"	setup Simplifier.setup
-			setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
-                        setup Splitter.setup setup Clasimp.setup
-			setup rulify_attrib_setup
+use "blastdata.ML"
+setup Blast.setup
 
+use "simpdata.ML"
+setup Simplifier.setup
+setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
+setup Splitter.setup setup Clasimp.setup
+setup rulify_attrib_setup
+
+use "meson_lemmas.ML"
 use "Tools/meson.ML"
+setup meson_setup
 
 end