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