src/HOL/Library/Z2.thy
changeset 70351 32b4e1aec5ca
parent 70342 e4d626692640
     1.1 --- a/src/HOL/Library/Z2.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Library/Z2.thy	Fri Jun 14 12:29:50 2019 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  text \<open>
     1.6    Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the
     1.7 -  type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper
     1.8 +  type provided here, for historical reasons named \<^text>\<open>bit\<close>, is only needed if proper
     1.9    field operations are required.
    1.10  \<close>
    1.11