--- a/src/HOL/Real.thy Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Real.thy Fri Jun 12 08:53:23 2015 +0200
@@ -438,7 +438,7 @@
"x - y = (x::real) + - y"
definition
- "divide x y = (x::real) * inverse y"
+ "x div y = (x::real) * inverse y"
lemma add_Real:
assumes X: "cauchy X" and Y: "cauchy Y"
@@ -501,7 +501,7 @@
apply (rule_tac x=k in exI, clarify)
apply (drule_tac x=n in spec, simp)
done
- show "divide a b = a * inverse b"
+ show "a div b = a * inverse b"
by (rule divide_real_def)
show "inverse (0::real) = 0"
by transfer (simp add: realrel_def)