# HG changeset patch
# User haftmann
# Date 1560508190 -7200
# Node ID 32b4e1aec5ca5840de7af1d4e26b7cec718c67e6
# Parent  571ae57313a494bc280ea8278385d52426b7656f
make latex happy

diff -r 571ae57313a4 -r 32b4e1aec5ca src/HOL/Library/Z2.thy
--- 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>