src/Pure/Isar/skip_proof.ML
changeset 12055 a9c44895cc8c
parent 11972 15da572c3c27
child 12148 a57873aec3bf
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Nov 05 20:58:28 2001 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Nov 05 20:59:35 2001 +0100
     1.3 @@ -12,8 +12,8 @@
     1.4    val make_thm: theory -> term -> thm
     1.5    val cheat_tac: theory -> tactic
     1.6    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.7 -  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     1.8 -    -> Proof.state -> Proof.state Seq.seq
     1.9 +  val local_skip_proof: (Proof.context -> {kind: string, name: string, thm: thm} -> unit) *
    1.10 +    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.11    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.12    val setup: (theory -> theory) list
    1.13  end;