src/Pure/Isar/skip_proof.ML
changeset 12244 179f142ffb03
parent 12148 a57873aec3bf
child 12318 72348ff7d4a0
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Nov 19 20:47:57 2001 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Nov 19 23:37:01 2001 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.5    val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
     1.6      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
     1.7 -  val global_skip_proof: Proof.state -> theory * (string * (string * thm list) list)
     1.8 +  val global_skip_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
     1.9    val setup: (theory -> theory) list
    1.10  end;
    1.11