# HG changeset patch # User wenzelm # Date 927751508 -7200 # Node ID a0b2cfa12d0d1cf7b9005d560107289befecfdb2 # Parent e5138b3dbd3bafaca78c3245afafa2d1b66f90b1 local_qed: print_result; diff -r e5138b3dbd3b -r a0b2cfa12d0d src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed May 26 22:44:41 1999 +0200 +++ b/src/Pure/Isar/method.ML Wed May 26 22:45:08 1999 +0200 @@ -55,10 +55,14 @@ val tac: text -> Proof.state -> Proof.state Seq.seq val then_tac: text -> Proof.state -> Proof.state Seq.seq val proof: text option -> Proof.state -> Proof.state Seq.seq - val local_qed: text option -> bool -> Proof.state -> Proof.state Seq.seq - val local_terminal_proof: text -> bool -> Proof.state -> Proof.state Seq.seq - val local_immediate_proof: bool -> Proof.state -> Proof.state Seq.seq - val local_default_proof: bool -> Proof.state -> Proof.state Seq.seq + val local_qed: text option -> ({kind: string, name: string, thm: thm} -> unit) + -> Proof.state -> Proof.state Seq.seq + val local_terminal_proof: text -> ({kind: string, name: string, thm: thm} -> unit) + -> Proof.state -> Proof.state Seq.seq + val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) + -> Proof.state -> Proof.state Seq.seq + val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) + -> Proof.state -> Proof.state Seq.seq val global_qed: bstring option -> theory attribute list option -> text option -> Proof.state -> theory * {kind: string, name: string, thm: thm} val global_terminal_proof: text -> Proof.state -> theory * {kind: string, name: string, thm: thm} @@ -301,7 +305,7 @@ |> Seq.map Proof.enter_forward; fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text)); -fun local_terminal_proof text int = Seq.THEN (proof (Some text), local_qed None int); +fun local_terminal_proof text pr = Seq.THEN (proof (Some text), local_qed None pr); val local_immediate_proof = local_terminal_proof (Basic (K same)); val local_default_proof = local_terminal_proof default_text;