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.
removed export_chain;
authorwenzelm
Wed, 15 Mar 2000 18:33:41 +0100
changeset 8466 f7b06595d0c8
parent 8465 df6549f5a01f
child 8467 58dbeea60bb8
removed export_chain;
src/Pure/Isar/isar_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_thy.ML	Wed Mar 15 18:32:41 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 15 18:33:41 2000 +0100
@@ -74,7 +74,6 @@
   val with_facts_i: (thm * Proof.context attribute list) list * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
-  val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
   val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
@@ -281,7 +280,6 @@
 val with_facts_i = gen_from_facts (gen_have_thmss_i add_thmss) o Comment.ignore;
 
 fun chain comment_ignore = ProofHistory.apply Proof.chain;
-fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain;
 
 
 (* context *)
isabelle