src/HOL/Rat.thy

 subsection \<open>The Set of Rational Numbers\<close>
 
 context field_char_0
 begin
 
-definition Rats :: "'a set" ("\<rat>")
+definition Rats :: "'a set" (\<open>\<rat>\<close>)
   where "\<rat> = range of_rat"
 
 end
 
 lemma Rats_cases [cases set: Rats]:

   uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
 
 
 subsection \<open>Float syntax\<close>
 
-syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
+syntax "_Float" :: "float_const \<Rightarrow> 'a"    (\<open>_\<close>)
 
 parse_translation \<open>
   let
     fun mk_frac str =
       let