src/HOL/Library/Extended.thy

 declare one_extended_def[symmetric, code_post]
 
 instantiation extended :: (plus)plus
 begin
 
-text {* The following definition of of addition is totalized
-to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *}
+text \<open>The following definition of of addition is totalized
+to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined.\<close>
 
 fun plus_extended where
 "Fin x + Fin y = Fin(x+y)" |
 "Fin x + Pinf  = Pinf" |
 "Pinf  + Fin x = Pinf" |

   "Minf  - Minf  = Pinf"
   "Pinf  - Pinf  = Pinf"
 by (simp_all add: minus_extended_def)
 
 
-text{* Numerals: *}
+text\<open>Numerals:\<close>
 
 instance extended :: ("{ab_semigroup_add,one}")numeral ..
 
 lemma Fin_numeral[code_post]: "Fin(numeral w) = numeral w"
   apply (induct w rule: num_induct)