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: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm |
12 val prove: ProofContext.context -> |
|
13 string list -> term list -> term -> (thm list -> tactic) -> thm |
13 end; |
14 end; |
14 |
15 |
15 structure SkipProof: SKIP_PROOF = |
16 structure SkipProof: SKIP_PROOF = |
16 struct |
17 struct |
17 |
18 |
32 Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop); |
33 Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop); |
33 |
34 |
34 fun cheat_tac thy st = |
35 fun cheat_tac thy st = |
35 ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st; |
36 ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st; |
36 |
37 |
37 fun prove thy xs asms prop tac = |
38 fun prove ctxt xs asms prop tac = |
38 Goal.prove thy xs asms prop |
39 Goal.prove ctxt xs asms prop |
39 (if ! quick_and_dirty then (K (cheat_tac thy)) else tac); |
40 (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac); |
40 |
41 |
41 end; |
42 end; |