--- a/src/Pure/Isar/isar_syn.ML Tue Jul 06 21:06:03 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jul 06 21:06:51 1999 +0200
@@ -396,18 +396,6 @@
OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
-val prevP =
- OuterSyntax.improper_command "prev" "previous proof state" K.control
- (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
-
-val upP =
- OuterSyntax.improper_command "up" "upper proof state" K.control
- (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
-
-val topP =
- OuterSyntax.improper_command "top" "to initial proof state" K.control
- (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
-
(* history *)
@@ -565,7 +553,7 @@
fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
- prevP, upP, topP, cannot_undoP, clear_undoP, redoP, undos_proofP,
+ cannot_undoP, clear_undoP, redoP, undos_proofP,
kill_proofP, undoP,
(*diagnostic commands*)
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
--- a/src/Pure/Isar/isar_thy.ML Tue Jul 06 21:06:03 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML Tue Jul 06 21:06:51 1999 +0200
@@ -271,35 +271,34 @@
fun global_statement_i f (name, atts, t) int thy =
ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy);
-fun local_statement do_open f g (name, src, s) = ProofHistory.apply_cond_open do_open (fn state =>
+fun local_statement f g (name, src, s) = ProofHistory.apply (fn state =>
f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
-fun local_statement_i do_open f g (name, atts, t) =
- ProofHistory.apply_cond_open do_open (f name atts t o g);
+fun local_statement_i f g (name, atts, t) = ProofHistory.apply (f name atts t o g);
val theorem = global_statement Proof.theorem o Comment.ignore;
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 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;
-val have_i = local_statement_i true Proof.have_i I o Comment.ignore;
-val thus = local_statement true Proof.show Proof.chain o Comment.ignore;
-val thus_i = local_statement_i true Proof.show_i Proof.chain o Comment.ignore;
-val hence = local_statement true Proof.have Proof.chain o Comment.ignore;
-val hence_i = local_statement_i true Proof.have_i Proof.chain o Comment.ignore;
+val assume = local_statement (Proof.assume assume_tac) I o Comment.ignore;
+val assume_i = local_statement_i (Proof.assume_i assume_tac) I o Comment.ignore;
+val presume = local_statement (Proof.assume (K all_tac)) I o Comment.ignore;
+val presume_i = local_statement_i (Proof.assume_i (K all_tac)) I o Comment.ignore;
+val show = local_statement Proof.show I o Comment.ignore;
+val show_i = local_statement_i Proof.show_i I o Comment.ignore;
+val have = local_statement Proof.have I o Comment.ignore;
+val have_i = local_statement_i Proof.have_i I o Comment.ignore;
+val thus = local_statement Proof.show Proof.chain o Comment.ignore;
+val thus_i = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
+val hence = local_statement Proof.have Proof.chain o Comment.ignore;
+val hence_i = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
(* blocks *)
-val begin_block = ProofHistory.apply_open Proof.begin_block;
+val begin_block = ProofHistory.apply Proof.begin_block;
val next_block = ProofHistory.apply Proof.next_block;
-val end_block = ProofHistory.apply_close Proof.end_block;
+val end_block = ProofHistory.apply Proof.end_block;
(* backward steps *)
@@ -325,14 +324,14 @@
(* local endings *)
val local_qed =
- proof'' o (ProofHistory.applys_close oo Method.local_qed) o apsome Comment.ignore_interest;
+ proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
val local_terminal_proof =
- proof'' o (ProofHistory.applys_close oo Method.local_terminal_proof) o Comment.ignore_interest;
+ proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o Comment.ignore_interest;
-val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
-val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
-val local_skip_proof = proof'' (ProofHistory.applys_close o SkipProof.local_skip_proof);
+val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
+val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
+val local_skip_proof = proof'' (ProofHistory.applys o SkipProof.local_skip_proof);
(* global endings *)