equal
deleted
inserted
replaced
314 |
314 |
315 ML{*local |
315 ML{*local |
316 fun mk_tac tac = |
316 fun mk_tac tac = |
317 timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})]) |
317 timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})]) |
318 in |
318 in |
319 val c_tac = mk_tac (add_tac @{context}) |
319 val c_tac = mk_tac (add_tac @{context}) |
320 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
320 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) |
321 end*} |
321 end*} |
322 |
322 |
323 text {* |
323 text {* |
324 This is all we need to let the conversion run against the simproc: |
324 This is all we need to let the conversion run against the simproc: |
325 *} |
325 *} |