equal
deleted
inserted
replaced
21 |
21 |
22 fun skip_proof (_, SkipProof prop) = |
22 fun skip_proof (_, SkipProof prop) = |
23 if ! quick_and_dirty then prop |
23 if ! quick_and_dirty then prop |
24 else error "Proof may be skipped in quick_and_dirty mode only!"; |
24 else error "Proof may be skipped in quick_and_dirty mode only!"; |
25 |
25 |
26 val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)]; |
26 val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof)); |
27 |
27 |
28 |
28 |
29 (* basic cheating *) |
29 (* basic cheating *) |
30 |
30 |
31 fun make_thm thy prop = |
31 fun make_thm thy prop = |