src/Pure/Isar/skip_proof.ML
changeset 6984 26d43e26ea61
parent 6935 a3f3f4128cab
child 8539 3cbe48a112f7
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Jul 12 22:28:38 1999 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Jul 12 22:28:56 1999 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature SKIP_PROOF =
     1.6  sig
     1.7 -  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit)
     1.8 +  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
     1.9      -> Proof.state -> Proof.state Seq.seq
    1.10    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.11    val setup: (theory -> theory) list