src/HOL/Number_Theory/Totient.thy

   also have "{1..n} = (\<Union>d\<in>{d. d dvd n}. A d)" by safe (auto simp: A_def)
   also have "card \<dots> = (\<Sum>d | d dvd n. card (A d))"
     using \<open>n > 0\<close> by (intro card_UN_disjoint) (auto simp: A_def)
   also have "\<dots> = (\<Sum>d | d dvd n. totient (n div d))" by (intro sum.cong refl *) auto
   also have "\<dots> = (\<Sum>d | d dvd n. totient d)" using \<open>n > 0\<close>
-    by (intro sum.reindex_bij_witness[of _ "op div n" "op div n"]) (auto elim: dvdE)
+    by (intro sum.reindex_bij_witness[of _ "(div) n" "(div) n"]) (auto elim: dvdE)
   finally show ?thesis ..
 qed auto
 
 lemma totient_mult_coprime:
   assumes "coprime m n"

 
 lemma totient_prime_power_Suc:
   assumes "prime p"
   shows   "totient (p ^ Suc n) = p ^ n * (p - 1)"
 proof -
-  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - op * p ` {0<..p ^ n})"
+  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - ( * ) p ` {0<..p ^ n})"
     unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
-  also from assms have "\<dots> = p ^ Suc n - card (op * p ` {0<..p^n})"
+  also from assms have "\<dots> = p ^ Suc n - card (( * ) p ` {0<..p^n})"
     by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
-  also from assms have "card (op * p ` {0<..p^n}) = p ^ n"
+  also from assms have "card (( * ) p ` {0<..p^n}) = p ^ n"
     by (subst card_image) (auto simp: inj_on_def)
   also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
   finally show ?thesis .
 qed