changeset 352 | 9f12e53eb121 |
parent 351 | f118240ab44a |
child 391 | ae2f0b40c840 |
--- a/ProgTutorial/Solutions.thy Sun Oct 18 21:22:44 2009 +0200 +++ b/ProgTutorial/Solutions.thy Mon Oct 19 02:02:21 2009 +0200 @@ -316,8 +316,8 @@ fun mk_tac tac = timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})]) in -val c_tac = mk_tac (add_tac @{context}) -val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) + val c_tac = mk_tac (add_tac @{context}) + val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) end*} text {*