src/HOL/Rat.thy
changeset 60429 d3d1e185cd63
parent 60352 d46de31a50c4
child 60688 01488b559910
     1.1 --- a/src/HOL/Rat.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Rat.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -162,9 +162,9 @@
     1.4    by transfer simp
     1.5  
     1.6  definition
     1.7 -  divide_rat_def: "divide q r = q * inverse (r::rat)"
     1.8 +  divide_rat_def: "q div r = q * inverse (r::rat)"
     1.9  
    1.10 -lemma divide_rat [simp]: "divide (Fract a b) (Fract c d) = Fract (a * d) (b * c)"
    1.11 +lemma divide_rat [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)"
    1.12    by (simp add: divide_rat_def)
    1.13  
    1.14  instance proof
    1.15 @@ -191,7 +191,7 @@
    1.16      by transfer simp
    1.17    { assume "q \<noteq> 0" thus "inverse q * q = 1"
    1.18      by transfer simp }
    1.19 -  show "divide q r = q * inverse r"
    1.20 +  show "q div r = q * inverse r"
    1.21      by (fact divide_rat_def)
    1.22    show "inverse 0 = (0::rat)"
    1.23      by transfer simp