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.
discontinued Proofterm.Promise (cf. 725438ceae7c);
authorwenzelm
Tue, 23 Jul 2019 19:07:28 +0200
changeset 70401 3c9f6aad092f
parent 70400 65bbef66e2ec
child 70402 29d81b53c40b
discontinued Proofterm.Promise (cf. 725438ceae7c);
src/Doc/Implementation/Logic.thy file | annotate | diff | comparison | revisions 
--- a/src/Doc/Implementation/Logic.thy	Tue Jul 23 19:04:56 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Jul 23 19:07:28 2019 +0200
@@ -1191,8 +1191,8 @@
   \<^descr> Type \<^ML_type>\<open>proof\<close> represents proof terms; this is a datatype with
   constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
   @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
-  Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML Promise}, @{index_ML
-  PThm} as explained above. %FIXME OfClass (!?)
+  Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
+  above. %FIXME OfClass (!?)
 
   \<^descr> Type \<^ML_type>\<open>proof_body\<close> represents the nested proof information of a
   named theorem, consisting of a digest of oracles and named theorem over some
isabelle