src/HOL/Import/HOL_Light_Maps.thy

 lemma [import_const T]:
   "True = ((\<lambda>p :: bool. p) = (\<lambda>p. p))"
   by simp
 
 lemma [import_const "/\\"]:
-  "(op \<and>) = (\<lambda>p q. (\<lambda>f. f p q :: bool) = (\<lambda>f. f True True))"
+  "(\<and>) = (\<lambda>p q. (\<lambda>f. f p q :: bool) = (\<lambda>f. f True True))"
   by metis
 
 lemma [import_const "==>"]:
-  "(op \<longrightarrow>) = (\<lambda>(p::bool) q::bool. (p \<and> q) = p)"
+  "(\<longrightarrow>) = (\<lambda>(p::bool) q::bool. (p \<and> q) = p)"
   by auto
 
 lemma [import_const "!"]:
   "All = (\<lambda>P::'A \<Rightarrow> bool. P = (\<lambda>x::'A. True))"
   by auto

 lemma [import_const "?"]:
   "Ex = (\<lambda>P::'A \<Rightarrow> bool. All (\<lambda>q::bool. (All (\<lambda>x::'A::type. (P x) \<longrightarrow> q)) \<longrightarrow> q))"
   by auto
 
 lemma [import_const "\\/"]:
-  "(op \<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)"
+  "(\<or>) = (\<lambda>p q. \<forall>r. (p \<longrightarrow> r) \<longrightarrow> (q \<longrightarrow> r) \<longrightarrow> r)"
   by auto
 
 lemma [import_const F]:
   "False = (\<forall>p. p)"
   by auto

 lemma [import_const COND]:
   "If = (\<lambda>t (t1 :: 'A) t2. SOME x. (t = True \<longrightarrow> x = t1) \<and> (t = False \<longrightarrow> x = t2))"
   unfolding fun_eq_iff by auto
 
 lemma [import_const o]:
-  "(op \<circ>) = (\<lambda>(f::'B \<Rightarrow> 'C) g x::'A. f (g x))"
+  "(\<circ>) = (\<lambda>(f::'B \<Rightarrow> 'C) g x::'A. f (g x))"
   unfolding fun_eq_iff by simp
 
 lemma [import_const I]: "id = (\<lambda>x::'A. x)"
   by auto
 

 lemma LT[import_const "<" : less]:
   "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
   by auto
 
 lemma DEF_GE[import_const ">=" : greater_eq]:
-  "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
+  "(\<ge>) = (\<lambda>x y :: nat. y \<le> x)"
   by simp
 
 lemma DEF_GT[import_const ">" : greater]:
-  "(op >) = (\<lambda>x y :: nat. y < x)"
+  "(>) = (\<lambda>x y :: nat. y < x)"
   by simp
 
 lemma DEF_MAX[import_const "MAX"]:
   "max = (\<lambda>x y :: nat. if x \<le> y then y else x)"
   by (auto simp add: max.absorb_iff2 fun_eq_iff)