Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 54093 4e299e2c762d
parent 53764 eba0d1c069b8
child 54495 237d5be57277 
--- 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