
diff -r 5e9de4faef98 -r d3d1e185cd63 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -241,9 +241,9 @@
     by (simp add: Fract_def inverse_fract_def UN_fractrel)
 qed
 
-definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
+definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)"
 
-lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
+lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
 
 instance
@@ -255,7 +255,7 @@
       (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)




