| changeset 6854 | 60a5ee0ca81d |
| parent 6746 | cf6ad8d22793 |
| child 6944 | 214e41d27d74 |
--- a/src/HOL/Isar_examples/NatSum.thy Mon Jun 28 23:02:38 1999 +0200 +++ b/src/HOL/Isar_examples/NatSum.thy Mon Jun 28 23:05:19 1999 +0200 @@ -35,10 +35,10 @@ theorem "2 * sum (%i. i) (Suc n) = n * Suc n"; proof same; - refine simp_tac; - refine (induct n); - refine simp_tac; - refine asm_simp_tac; + apply simp_tac; + apply (induct n); + apply simp_tac; + apply asm_simp_tac; qed_with sum_of_naturals;