changeset 225 | 7859fc59249a |
parent 214 | 7e04dc2368b0 |
child 239 | b63c72776f03 |
child 270 | bfcabed9079e |
--- a/ProgTutorial/Solutions.thy Wed Apr 01 15:42:47 2009 +0100 +++ b/ProgTutorial/Solutions.thy Thu Apr 02 11:48:35 2009 +0100 @@ -187,7 +187,8 @@ *} ML{*local - fun mk_tac tac = timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})]) + fun mk_tac tac = + timing_wrapper (EVERY1 [tac, K (SkipProof.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}]))