equal
deleted
inserted
replaced
13 val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm |
13 val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm |
14 val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) * |
14 val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) * |
15 (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq |
15 (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq |
16 val global_skip_proof: |
16 val global_skip_proof: |
17 bool -> Proof.state -> theory * ((string * string) * (string * thm list) list) |
17 bool -> Proof.state -> theory * ((string * string) * (string * thm list) list) |
18 val setup: (theory -> theory) list |
|
19 end; |
18 end; |
20 |
19 |
21 structure SkipProof: SKIP_PROOF = |
20 structure SkipProof: SKIP_PROOF = |
22 struct |
21 struct |
23 |
22 |
36 |
35 |
37 fun skip_proof (_, SkipProof t) = |
36 fun skip_proof (_, SkipProof t) = |
38 if ! quick_and_dirty then t |
37 if ! quick_and_dirty then t |
39 else error "Proof may be skipped in quick_and_dirty mode only!"; |
38 else error "Proof may be skipped in quick_and_dirty mode only!"; |
40 |
39 |
41 val setup = |
40 val _ = Context.add_setup |
42 [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path]; |
41 [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path]; |
43 |
42 |
44 |
43 |
45 (* basic cheating *) |
44 (* basic cheating *) |
46 |
45 |
47 fun make_thm thy t = |
46 fun make_thm thy t = |