src/Doc/Isar_Ref/Generic.thy

   Ordered rewriting with the combination of A, C, and LC sorts a term
   lexicographically --- the rewriting engine imitates bubble-sort.
 \<close>
 
 experiment
-  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<bullet>" 60)
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix \<open>\<bullet>\<close> 60)
   assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
   assumes commute: "x \<bullet> y = y \<bullet> x"
 begin
 
 lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)"