ProgTutorial/Recipes/Timing.thy
changeset 456 89fccd3d5055
parent 346 0fea8b7a14a1
child 460 5c33c4b52ad7
--- 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