src/HOL/HOL.thy
changeset 9839 da5ca8b30244
parent 9736 332fab43628f
child 9852 6ca7fcac3e23
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 05 10:13:20 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 05 10:14:36 2000 +0200
     1.3 @@ -7,7 +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 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") 
     1.9 +      ("Tools/meson.ML"):
    1.10  
    1.11  
    1.12  (** Core syntax **)
    1.13 @@ -221,4 +222,6 @@
    1.14                          setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup
    1.15  			setup attrib_setup
    1.16  
    1.17 +use "Tools/meson.ML"
    1.18 +
    1.19  end