src/HOL/Library/Fraction_Field.thy
changeset 60429 d3d1e185cd63
parent 60352 d46de31a50c4
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -241,9 +241,9 @@
     1.4      by (simp add: Fract_def inverse_fract_def UN_fractrel)
     1.5  qed
     1.6  
     1.7 -definition divide_fract_def: "divide q r = q * inverse (r:: 'a fract)"
     1.8 +definition divide_fract_def: "q div r = q * inverse (r:: 'a fract)"
     1.9  
    1.10 -lemma divide_fract [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
    1.11 +lemma divide_fract [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
    1.12    by (simp add: divide_fract_def)
    1.13  
    1.14  instance
    1.15 @@ -255,7 +255,7 @@
    1.16        (simp_all add: fract_expand eq_fract mult.commute)
    1.17  next
    1.18    fix q r :: "'a fract"
    1.19 -  show "divide q r = q * inverse r" by (simp add: divide_fract_def)
    1.20 +  show "q div r = q * inverse r" by (simp add: divide_fract_def)
    1.21  next
    1.22    show "inverse 0 = (0:: 'a fract)"
    1.23      by (simp add: fract_expand) (simp add: fract_collapse)