changeset 35967 | b9659daa5b4b |
parent 35867 | 16279c4c7a33 |
child 36062 | 194cb6e3c13f |
--- a/src/HOL/Sledgehammer.thy Wed Mar 24 12:30:33 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Wed Mar 24 12:31:37 2010 +0100 @@ -12,6 +12,7 @@ uses "Tools/polyhash.ML" "~~/src/Tools/Metis/metis.ML" + "Tools/Sledgehammer/sledgehammer_util.ML" ("Tools/Sledgehammer/sledgehammer_fol_clause.ML") ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML") ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")