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