equal
deleted
inserted
replaced
149 fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i))); |
149 fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i))); |
150 |
150 |
151 |
151 |
152 (* cheating *) |
152 (* cheating *) |
153 |
153 |
154 fun cheating int ctxt = METHOD (K (setmp_CRITICAL quick_and_dirty (int orelse ! quick_and_dirty) |
154 fun cheating int ctxt = |
155 (SkipProof.cheat_tac (ProofContext.theory_of ctxt)))); |
155 if int orelse ! quick_and_dirty then |
|
156 METHOD (K (Skip_Proof.cheat_tac (ProofContext.theory_of ctxt))) |
|
157 else error "Cheating requires quick_and_dirty mode!"; |
156 |
158 |
157 |
159 |
158 (* unfold intro/elim rules *) |
160 (* unfold intro/elim rules *) |
159 |
161 |
160 fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths)); |
162 fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths)); |