1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 28 12:32:38 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 28 15:26:32 2005 +0200
     1.3 @@ -166,7 +166,7 @@
     1.4  by arith
     1.5  
     1.6  lemma "abs (2*x) = 2 * abs (x :: int)"
     1.7 -by (simp add: zabs_def) 
     1.8 +by (simp add: abs_if) 
     1.9  
    1.10  
    1.11  text {*Induction rules for the Integers