equal
deleted
inserted
replaced
185 respectively. The idea is to first apply the conversion (respectively simproc) and |
185 respectively. The idea is to first apply the conversion (respectively simproc) and |
186 then prove the remaining goal using @{ML "cheat_tac" in SkipProof}. |
186 then prove the remaining goal using @{ML "cheat_tac" in SkipProof}. |
187 *} |
187 *} |
188 |
188 |
189 ML{*local |
189 ML{*local |
190 fun mk_tac tac = timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})]) |
190 fun mk_tac tac = |
|
191 timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})]) |
191 in |
192 in |
192 val c_tac = mk_tac (add_tac @{context}) |
193 val c_tac = mk_tac (add_tac @{context}) |
193 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
194 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
194 end*} |
195 end*} |
195 |
196 |