src/HOL/Number_Theory/Gauss.thy

     by (auto simp add: B_def inj_on_def A_def) metis
 qed
 
 lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
   apply (auto simp add: E_def C_def B_def A_def)
-  apply (rule inj_on_inverseI [where g = "op - (int p)"])
+  apply (rule inj_on_inverseI [where g = "(-) (int p)"])
   apply auto
   done
 
 lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
   for x :: int

 lemma prod_D_F_eq_prod_A: "prod id D * prod id F = prod id A"
   by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F prod.union_disjoint)
 
 lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * prod id E] (mod p)"
 proof -
-  have FE: "prod id F = prod (op - p) E"
+  have FE: "prod id F = prod ((-) p) E"
     apply (auto simp add: F_def)
     apply (insert finite_E inj_on_pminusx_E)
     apply (drule prod.reindex)
     apply auto
     done
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
     by (metis cong_def minus_mod_self1 mod_mod_trivial)
-  then have "[prod ((\<lambda>x. x mod p) \<circ> (op - p)) E = prod (uminus) E](mod p)"
-    using finite_E p_ge_2 cong_prod [of E "(\<lambda>x. x mod p) \<circ> (op - p)" uminus p]
+  then have "[prod ((\<lambda>x. x mod p) \<circ> ((-) p)) E = prod (uminus) E](mod p)"
+    using finite_E p_ge_2 cong_prod [of E "(\<lambda>x. x mod p) \<circ> ((-) p)" uminus p]
     by auto
   then have two: "[prod id F = prod (uminus) E](mod p)"
     by (metis FE cong_cong_mod_int cong_refl cong_prod minus_mod_self1)
   have "prod uminus E = (-1) ^ card E * prod id E"
     using finite_E by (induct set: finite) auto