src/HOL/Real.thy
changeset 60429 d3d1e185cd63
parent 60352 d46de31a50c4
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Real.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Real.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -438,7 +438,7 @@
     1.4    "x - y = (x::real) + - y"
     1.5  
     1.6  definition
     1.7 -  "divide x y = (x::real) * inverse y"
     1.8 +  "x div y = (x::real) * inverse y"
     1.9  
    1.10  lemma add_Real:
    1.11    assumes X: "cauchy X" and Y: "cauchy Y"
    1.12 @@ -501,7 +501,7 @@
    1.13      apply (rule_tac x=k in exI, clarify)
    1.14      apply (drule_tac x=n in spec, simp)
    1.15      done
    1.16 -  show "divide a b = a * inverse b"
    1.17 +  show "a div b = a * inverse b"
    1.18      by (rule divide_real_def)
    1.19    show "inverse (0::real) = 0"
    1.20      by transfer (simp add: realrel_def)