1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Tue Apr 29 16:00:34 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Tue Apr 29 16:02:02 2014 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    The term @{term "Suc n"} is no longer a valid pattern.  Therefore,
     1.5    all occurrences of this term in a position where a pattern is
     1.6    expected (i.e.~on the left-hand side of a code equation) must be
     1.7 -  eliminated.  This can be accomplished – as far as possible – by
     1.8 +  eliminated.  This can be accomplished -- as far as possible -- by
     1.9    applying the following transformation rule:
    1.10  *}
    1.11