--- a/src/Pure/Isar/isar_thy.ML Mon Jun 28 21:47:04 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML Mon Jun 28 21:47:55 1999 +0200
@@ -79,6 +79,10 @@
-> ProofHistory.T -> ProofHistory.T
val assume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
-> ProofHistory.T -> ProofHistory.T
+ val presume: (string * Args.src list * (string * string list) list) * Comment.text
+ -> ProofHistory.T -> ProofHistory.T
+ val presume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
+ -> ProofHistory.T -> ProofHistory.T
val show: (string * Args.src list * (string * string list)) * Comment.text
-> ProofHistory.T -> ProofHistory.T
val show_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
@@ -259,8 +263,10 @@
val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
val lemma = global_statement Proof.lemma o Comment.ignore;
val lemma_i = global_statement_i Proof.lemma_i o Comment.ignore;
-val assume = local_statement false Proof.assume I o Comment.ignore;
-val assume_i = local_statement_i false Proof.assume_i I o Comment.ignore;
+val assume = local_statement false (Proof.assume assume_tac) I o Comment.ignore;
+val assume_i = local_statement_i false (Proof.assume_i assume_tac) I o Comment.ignore;
+val presume = local_statement false (Proof.assume (K all_tac)) I o Comment.ignore;
+val presume_i = local_statement_i false (Proof.assume_i (K all_tac)) I o Comment.ignore;
val show = local_statement true Proof.show I o Comment.ignore;
val show_i = local_statement_i true Proof.show_i I o Comment.ignore;
val have = local_statement true Proof.have I o Comment.ignore;