src/CCL/Term.thy

   mkall_dstnct_thms @{context} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
     [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
 \<close>
 
 
-subsection \<open>Rules for pre-order @{text "[="}\<close>
+subsection \<open>Rules for pre-order \<open>[=\<close>\<close>
 
 lemma term_porews:
   "inl(a) [= inl(a') \<longleftrightarrow> a [= a'"
   "inr(b) [= inr(b') \<longleftrightarrow> b [= b'"
   "succ(n) [= succ(n') \<longleftrightarrow> n [= n'"