src/HOL/Hahn_Banach/Bounds.thy

 (*  Title:      HOL/Hahn_Banach/Bounds.thy
     Author:     Gertrud Bauer, TU Munich
 *)
 
-header {* Bounds *}
+header \<open>Bounds\<close>
 
 theory Bounds
 imports Main "~~/src/HOL/Library/ContNotDenum"
 begin
 

   shows "\<Squnion>A = (x::'a::order)"
 proof -
   interpret lub A x by fact
   show ?thesis
   proof (unfold the_lub_def)
-    from `lub A x` show "The (lub A) = x"
+    from \<open>lub A x\<close> show "The (lub A) = x"
     proof
       fix x' assume lub': "lub A x'"
       show "x' = x"
       proof (rule order_antisym)
         from lub' show "x' \<le> x"