--- a/src/HOL/Library/Z2.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Library/Z2.thy Fri Jun 14 12:29:50 2019 +0200
@@ -10,7 +10,7 @@
text \<open>
Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the
- type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper
+ type provided here, for historical reasons named \<^text>\<open>bit\<close>, is only needed if proper
field operations are required.
\<close>