--- a/src/HOL/Rat.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Rat.thy Tue Aug 13 16:25:47 2013 +0200
@@ -409,9 +409,9 @@
assume "b \<noteq> 0" and "d \<noteq> 0" and "a * d = c * b"
hence "a * d * b * d = c * b * b * d"
by simp
- hence "a * b * d\<twosuperior> = c * d * b\<twosuperior>"
+ hence "a * b * d\<^sup>2 = c * d * b\<^sup>2"
unfolding power2_eq_square by (simp add: mult_ac)
- hence "0 < a * b * d\<twosuperior> \<longleftrightarrow> 0 < c * d * b\<twosuperior>"
+ hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
by simp
thus "0 < a * b \<longleftrightarrow> 0 < c * d"
using `b \<noteq> 0` and `d \<noteq> 0`