src/Pure/Isar/method.ML
changeset 6934 04d051190a5f
parent 6872 b250da153b1e
child 6951 13399b560e4e
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jul 08 18:35:11 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jul 08 18:35:44 1999 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4    val proof: text option -> Proof.state -> Proof.state Seq.seq
     1.5    val local_qed: text option -> ({kind: string, name: string, thm: thm} -> unit)
     1.6      -> Proof.state -> Proof.state Seq.seq
     1.7 -  val local_terminal_proof: text -> ({kind: string, name: string, thm: thm} -> unit)
     1.8 +  val local_terminal_proof: text * text option -> ({kind: string, name: string, thm: thm} -> unit)
     1.9      -> Proof.state -> Proof.state Seq.seq
    1.10    val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit)
    1.11      -> Proof.state -> Proof.state Seq.seq
    1.12 @@ -65,7 +65,8 @@
    1.13      -> Proof.state -> Proof.state Seq.seq
    1.14    val global_qed: bstring option -> theory attribute list option -> text option
    1.15      -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.16 -  val global_terminal_proof: text -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.17 +  val global_terminal_proof: text * text option
    1.18 +    -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.19    val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.20    val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.21    val setup: (theory -> theory) list
    1.22 @@ -306,9 +307,9 @@
    1.23    |> Seq.map Proof.enter_forward;
    1.24  
    1.25  fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
    1.26 -fun local_terminal_proof text pr = Seq.THEN (proof (Some text), local_qed None pr);
    1.27 -val local_immediate_proof = local_terminal_proof (Basic (K same));
    1.28 -val local_default_proof = local_terminal_proof default_text;
    1.29 +fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);
    1.30 +val local_immediate_proof = local_terminal_proof (Basic (K same), None);
    1.31 +val local_default_proof = local_terminal_proof (default_text, None);
    1.32  
    1.33  
    1.34  fun global_qeds alt_name alt_atts opt_text =
    1.35 @@ -320,16 +321,16 @@
    1.36    |> Proof.check_result "Failed to finish proof" state
    1.37    |> Seq.hd;
    1.38  
    1.39 -fun global_terminal_proof text state =
    1.40 +fun global_terminal_proof (text, opt_text) state =
    1.41    state
    1.42    |> proof (Some text)
    1.43    |> Proof.check_result "Terminal proof method failed" state
    1.44 -  |> (Seq.flat o Seq.map (global_qeds None None None))
    1.45 +  |> (Seq.flat o Seq.map (global_qeds None None opt_text))
    1.46    |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
    1.47    |> Seq.hd;
    1.48  
    1.49 -val global_immediate_proof = global_terminal_proof (Basic (K same));
    1.50 -val global_default_proof = global_terminal_proof default_text;
    1.51 +val global_immediate_proof = global_terminal_proof (Basic (K same), None);
    1.52 +val global_default_proof = global_terminal_proof (default_text, None);
    1.53  
    1.54  
    1.55