# HG changeset patch # User griff # Date 1288351005 -7200 # Node ID 89fccd3d50556c6064bc783f3dae0604d09ac07c # Parent fcd0fb70994b92d54a48aa0231c2f818d6e7a565 'nat_number' was renamed to 'eval_nat_numeral' diff -r fcd0fb70994b -r 89fccd3d5055 ProgTutorial/Recipes/Timing.thy --- a/ProgTutorial/Recipes/Timing.thy Fri Oct 29 13:10:33 2010 +0200 +++ b/ProgTutorial/Recipes/Timing.thy Fri Oct 29 13:16:45 2010 +0200 @@ -52,7 +52,7 @@ lemma "ackermann (3, 4) = 125" apply(tactic {* - timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *}) + timing_wrapper (simp_tac (@{simpset} addsimps @{thms "eval_nat_numeral"}) 1) *}) done text {* @@ -69,4 +69,4 @@ -end \ No newline at end of file +end diff -r fcd0fb70994b -r 89fccd3d5055 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Fri Oct 29 13:10:33 2010 +0200 +++ b/ProgTutorial/Tactical.thy Fri Oct 29 13:16:45 2010 +0200 @@ -1989,7 +1989,7 @@ val num = HOLogic.mk_number @{typ "nat"} n val goal = Logic.mk_equals (t, num) val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ - @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps} + @{thms eval_nat_numeral} @ @{thms neg_simps} @ @{thms plus_nat.simps} in Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1)) end*}