equal
deleted
inserted
replaced
50 wrapper is the proof |
50 wrapper is the proof |
51 *} |
51 *} |
52 |
52 |
53 lemma "ackermann (3, 4) = 125" |
53 lemma "ackermann (3, 4) = 125" |
54 apply(tactic {* |
54 apply(tactic {* |
55 timing_wrapper (simp_tac (@{simpset} addsimps @{thms "eval_nat_numeral"}) 1) *}) |
55 timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1) *}) |
56 done |
56 done |
57 |
57 |
58 text {* |
58 text {* |
59 where it returns something on the scale of 3 seconds. We chose to return |
59 where it returns something on the scale of 3 seconds. We chose to return |
60 this information as a string, but the timing information is also accessible |
60 this information as a string, but the timing information is also accessible |