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.
no isar proofs if preplay was not attempted
authorblanchet
Wed, 09 Oct 2013 16:40:03 +0200
changeset 54093 4e299e2c762d
parent 54092 1e2585f56509
child 54094 5d077ce92d00
no isar proofs if preplay was not attempted
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 09 16:38:48 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 09 16:40:03 2013 +0200
@@ -640,7 +640,7 @@
 fun isar_proof_would_be_a_good_idea preplay =
   case preplay of
     Played (reconstr, _) => reconstr = SMT
-  | Trust_Playable _ => true
+  | Trust_Playable _ => false
   | Failed_to_Play _ => true
 
 fun proof_text ctxt isar_proofs isar_params num_chained
isabelle