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.
tuned;
authorwenzelm
Tue, 20 Aug 2019 15:24:07 +0200
changeset 70593 1d239ebba0e3
parent 70592 78426ea26f12
child 70594 64b5514c33b1
tuned;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/proofterm.ML	Tue Aug 20 15:12:06 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 15:24:07 2019 +0200
@@ -209,7 +209,7 @@
 val oracle_prop = the_default Term.dummy;
 
 type thm = serial * thm_node;
-val thm_ord : thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
+val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
 exception MIN_PROOF;
 
--- a/src/Pure/thm.ML	Tue Aug 20 15:12:06 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 20 15:24:07 2019 +0200
@@ -710,7 +710,7 @@
 
 (* inference rules *)
 
-fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
+val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
 fun deriv_rule2 f
     (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
isabelle