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.
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
authorwenzelm
Tue, 23 Jul 2019 23:10:22 +0200
changeset 70402 29d81b53c40b
parent 70401 3c9f6aad092f
child 70403 468cfd56ee03
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/proofterm.ML	Tue Jul 23 19:07:28 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 23 23:10:22 2019 +0200
@@ -394,6 +394,7 @@
   | AbsP _ => false
   | op % _ => false
   | op %% _ => false
+  | MinProof => false
   | _ => true);
 
 fun compact_proof (prf % _) = compact_proof prf
isabelle