Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compile
authorblanchet
Tue, 29 Jun 2010 11:14:52 +0200
changeset 37630 d30930f58006
parent 37629 a4f129820562
child 37631 16048a884a2c
compile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 29 11:03:26 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 29 11:14:52 2010 +0200
@@ -299,7 +299,6 @@
 
 fun run_sh prover hard_timeout timeout dir st =
   let
-    val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *)
     val {context = ctxt, facts, goal} = Proof.goal st
     val thy = ProofContext.theory_of ctxt
     val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
isabelle