| changeset 16585 | 02cf78f0afce |
| parent 16417 | 9bc16273c2d4 |
| child 22097 | 7ee0529c5674 |
--- a/doc-src/TutorialI/Types/Numbers.thy Tue Jun 28 12:32:38 2005 +0200 +++ b/doc-src/TutorialI/Types/Numbers.thy Tue Jun 28 15:26:32 2005 +0200 @@ -166,7 +166,7 @@ by arith lemma "abs (2*x) = 2 * abs (x :: int)" -by (simp add: zabs_def) +by (simp add: abs_if) text {*Induction rules for the Integers