added forget_proof;
authorwenzelm
Tue Feb 08 20:14:09 2000 +0100 (2000-02-08 ago)
changeset 8210ca3997312f47
parent 8209 4816ba139574
child 8211 714f164f0385
added forget_proof;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Feb 08 20:13:58 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 08 20:14:09 2000 +0100
     1.3 @@ -378,6 +378,11 @@
     1.4    OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
     1.5      (P.marg_comment >> IsarThy.skip_proof);
     1.6  
     1.7 +val forget_proofP =
     1.8 +  OuterSyntax.improper_command "oops" "forget proof" K.qed_global
     1.9 +    (P.marg_comment >> IsarThy.forget_proof);
    1.10 +
    1.11 +
    1.12  
    1.13  (* proof steps *)
    1.14  
    1.15 @@ -624,9 +629,9 @@
    1.16    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    1.17    defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
    1.18    nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    1.19 -  skip_proofP, deferP, preferP, applyP, then_applyP, proofP, alsoP,
    1.20 -  finallyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP,
    1.21 -  kill_proofP, undoP,
    1.22 +  skip_proofP, forget_proofP, deferP, preferP, applyP, then_applyP,
    1.23 +  proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
    1.24 +  undos_proofP, kill_proofP, undoP,
    1.25    (*diagnostic commands*)
    1.26    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.27    print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Feb 08 20:13:58 2000 +0100
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Feb 08 20:14:09 2000 +0100
     2.3 @@ -122,7 +122,6 @@
     2.4    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
     2.5    val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
     2.6      -> ProofHistory.T -> ProofHistory.T
     2.7 -  val kill_proof: ProofHistory.T -> theory
     2.8    val qed: (Method.text * Comment.interest) option * Comment.text
     2.9      -> Toplevel.transition -> Toplevel.transition
    2.10    val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
    2.11 @@ -130,6 +129,7 @@
    2.12    val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.13    val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.14    val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.15 +  val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
    2.16    val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
    2.17    val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
    2.18      -> Toplevel.transition -> Toplevel.transition
    2.19 @@ -402,8 +402,6 @@
    2.20  
    2.21  (* global endings *)
    2.22  
    2.23 -val kill_proof = Proof.theory_of o ProofHistory.current;
    2.24 -
    2.25  fun global_result finish = Toplevel.proof_to_theory (fn prf =>
    2.26    let
    2.27      val state = ProofHistory.current prf;
    2.28 @@ -426,6 +424,8 @@
    2.29  fun default_proof comment = local_default_proof o global_default_proof;
    2.30  fun skip_proof comment = local_skip_proof o global_skip_proof;
    2.31  
    2.32 +fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
    2.33 +
    2.34  
    2.35  (* calculational proof commands *)
    2.36