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.
renamed force_proof to join_proof;
authorwenzelm
Sat, 06 Dec 2008 00:09:01 +0100
changeset 29003 d8d3cbbb6fcc
parent 29002 c9cdb569487a
child 29009 3ad09b8d2534
renamed force_proof to join_proof;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/thm.ML	Sat Dec 06 00:08:32 2008 +0100
+++ b/src/Pure/thm.ML	Sat Dec 06 00:09:01 2008 +0100
@@ -149,7 +149,7 @@
   val future: thm future -> cterm -> thm
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
-  val force_proof: thm -> unit
+  val join_proof: thm -> unit
   val extern_oracles: theory -> xstring list
   val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
@@ -1638,7 +1638,7 @@
   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
 
 val proof_of = Proofterm.proof_of o proof_body_of;
-val force_proof = ignore o proof_body_of;
+val join_proof = ignore o proof_body_of;
 
 
 (* closed derivations with official name *)
isabelle