src/HOL/Real.thy
changeset 60352 d46de31a50c4
parent 60162 645058aa9d6f
child 60429 d3d1e185cd63
     1.1 --- a/src/HOL/Real.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Jun 01 18:59:21 2015 +0200
     1.3 @@ -438,7 +438,7 @@
     1.4    "x - y = (x::real) + - y"
     1.5  
     1.6  definition
     1.7 -  "x / y = (x::real) * inverse y"
     1.8 +  "divide x 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 "a / b = a * inverse b"
    1.17 +  show "divide a 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)