equal
deleted
inserted
replaced
7 |
7 |
8 signature SKIP_PROOF = |
8 signature SKIP_PROOF = |
9 sig |
9 sig |
10 val make_thm: theory -> term -> thm |
10 val make_thm: theory -> term -> thm |
11 val cheat_tac: theory -> tactic |
11 val cheat_tac: theory -> tactic |
12 val prove: ProofContext.context -> |
12 val prove: ProofContext.context -> string list -> term list -> term -> |
13 string list -> term list -> term -> (thm list -> tactic) -> thm |
13 ({prems: thm list, context: Context.proof} -> tactic) -> thm |
14 end; |
14 end; |
15 |
15 |
16 structure SkipProof: SKIP_PROOF = |
16 structure SkipProof: SKIP_PROOF = |
17 struct |
17 struct |
18 |
18 |