# 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*}