make latex happy
authorhaftmann
Fri Jun 14 12:29:50 2019 +0200 (4 months ago)
changeset 7035132b4e1aec5ca
parent 70350 571ae57313a4
child 70352 ce3c1d8791eb
make latex happy
src/HOL/Library/Z2.thy
     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