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.
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
authorwenzelm
Mon, 26 Apr 2010 21:36:44 +0200
changeset 36355 aaa9933039b3
parent 36354 bbd742107f56
child 36356 5ab0f8859f9f
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Mon Apr 26 20:30:50 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Apr 26 21:36:44 2010 +0200
@@ -661,6 +661,7 @@
     if immediate orelse
       null proof_trs orelse
       OuterKeyword.is_schematic_goal (name_of tr) orelse
+      exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
       not (can proof_of st') orelse
       Proof.is_relevant (proof_of st')
     then
isabelle