src/HOL/Library/Code_Abstract_Nat.thy
changeset 56790 f54097170704
parent 55757 9fc71814b8c1
child 57426 2cd2ccd81f93
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Tue Apr 29 16:00:34 2014 +0200
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Tue Apr 29 16:02:02 2014 +0200
@@ -34,7 +34,7 @@
   The term @{term "Suc n"} is no longer a valid pattern.  Therefore,
   all occurrences of this term in a position where a pattern is
   expected (i.e.~on the left-hand side of a code equation) must be
-  eliminated.  This can be accomplished – as far as possible – by
+  eliminated.  This can be accomplished -- as far as possible -- by
   applying the following transformation rule:
 *}