diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Meson.thy --- 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 *}