src/HOL/Library/Fraction_Field.thy

     by (auto simp add: congruent_def * algebra_simps)
   then show ?thesis
     by (simp add: Fract_def inverse_fract_def UN_fractrel)
 qed
 
-definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
-
-lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
+definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)"
+
+lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
 
 instance
 proof
   fix q :: "'a fract"

   then show "inverse q * q = 1"
     by (cases q rule: Fract_cases_nonzero)
       (simp_all add: fract_expand eq_fract mult.commute)
 next
   fix q r :: "'a fract"
-  show "divide q r = q * inverse r" by (simp add: divide_fract_def)
+  show "q div r = q * inverse r" by (simp add: divide_fract_def)
 next
   show "inverse 0 = (0:: 'a fract)"
     by (simp add: fract_expand) (simp add: fract_collapse)
 qed