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.
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
authorblanchet
Tue, 30 Sep 2014 14:18:07 +0200
changeset 58494 ed380b9594b5
parent 58493 308f3c7dfb67
child 58495 aefcb244423f
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Tue Sep 30 14:01:33 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Tue Sep 30 14:18:07 2014 +0200
@@ -228,7 +228,7 @@
     ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
     (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
      : prover_result) =
-  if is_some outcome orelse null used_facts then
+  if is_some outcome then
     result
   else
     let
isabelle