# HG changeset patch # User blanchet # Date 1286221832 -7200 # Node ID 1ae333bfef14a4184f7325c4187103fbe6f7f00c # Parent 02fcd9cd1eaca7fdf0d83c50c4a6d18ca9ee2bc8 remove Meson from Sledgehammer diff -r 02fcd9cd1eac -r 1ae333bfef14 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Oct 04 21:49:07 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Oct 04 21:50:32 2010 +0200 @@ -14,7 +14,6 @@ ("Tools/ATP/atp_proof.ML") ("Tools/ATP/atp_systems.ML") ("~~/src/Tools/Metis/metis.ML") - ("Tools/Sledgehammer/meson_clausify.ML") ("Tools/Sledgehammer/metis_translate.ML") ("Tools/Sledgehammer/metis_reconstruct.ML") ("Tools/Sledgehammer/metis_tactics.ML") @@ -104,9 +103,6 @@ setup ATP_Systems.setup use "~~/src/Tools/Metis/metis.ML" -use "Tools/Sledgehammer/meson_clausify.ML" -setup Meson_Clausify.setup - use "Tools/Sledgehammer/metis_translate.ML" use "Tools/Sledgehammer/metis_reconstruct.ML" use "Tools/Sledgehammer/metis_tactics.ML"