src/HOL/Library/Lattice_Algebras.thy

 (* Author: Steven Obua, TU Muenchen *)
 
-section {* Various algebraic structures combined with a lattice *}
+section \<open>Various algebraic structures combined with a lattice\<close>
 
 theory Lattice_Algebras
 imports Complex_Main
 begin
 

   then show ?thesis
     by (simp add: algebra_simps)
 qed
 
 
-subsection {* Positive Part, Negative Part, Absolute Value *}
+subsection \<open>Positive Part, Negative Part, Absolute Value\<close>
 
 definition nprt :: "'a \<Rightarrow> 'a"
   where "nprt x = inf x 0"
 
 definition pprt :: "'a \<Rightarrow> 'a"

     by (simp add: algebra_simps)
   have "- b \<le> \<bar>b\<bar>"
     by (rule abs_ge_minus_self)
   then have "c + (- b) \<le> c + \<bar>b\<bar>"
     by (rule add_left_mono)
-  with `a \<le> c + (- b)` show ?thesis
+  with \<open>a \<le> c + (- b)\<close> show ?thesis
     by (rule order_trans)
 qed
 
 class lattice_ring = ordered_ring + lattice_ab_group_add_abs
 begin