author | paulson |
Tue, 05 Sep 2000 10:14:36 +0200 | |
changeset 9839 | da5ca8b30244 |
parent 9838 | dc84dda48a5a |
child 9840 | 9dfcb0224f8c |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Tue Sep 05 10:13:20 2000 +0200 +++ b/src/HOL/HOL.thy Tue Sep 05 10:14:36 2000 +0200 @@ -7,7 +7,8 @@ *) theory HOL = CPure -files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"): +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") + ("Tools/meson.ML"): (** Core syntax **) @@ -221,4 +222,6 @@ setup Splitter.setup setup Clasimp.setup setup iff_attrib_setup setup attrib_setup +use "Tools/meson.ML" + end