src/HOL/Meson.thy
changeset 48891 c0eafbd55de3
parent 47953 a2c3706c4cb1
child 54148 c8cc5ab4a863
--- a/src/HOL/Meson.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Meson.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -9,9 +9,6 @@
 
 theory Meson
 imports Datatype
-uses ("Tools/Meson/meson.ML")
-     ("Tools/Meson/meson_clausify.ML")
-     ("Tools/Meson/meson_tactic.ML")
 begin
 
 subsection {* Negation Normal Form *}
@@ -194,9 +191,9 @@
 
 subsection {* Meson package *}
 
-use "Tools/Meson/meson.ML"
-use "Tools/Meson/meson_clausify.ML"
-use "Tools/Meson/meson_tactic.ML"
+ML_file "Tools/Meson/meson.ML"
+ML_file "Tools/Meson/meson_clausify.ML"
+ML_file "Tools/Meson/meson_tactic.ML"
 
 setup {* Meson_Tactic.setup *}