src/HOL/Rat.thy
changeset 53015 a1119cf551e8
parent 52146 ceb31e1ded30
child 53017 0f376701e83b
     1.1 --- a/src/HOL/Rat.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Rat.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -409,9 +409,9 @@
     1.4    assume "b \<noteq> 0" and "d \<noteq> 0" and "a * d = c * b"
     1.5    hence "a * d * b * d = c * b * b * d"
     1.6      by simp
     1.7 -  hence "a * b * d\<twosuperior> = c * d * b\<twosuperior>"
     1.8 +  hence "a * b * d\<^sup>2 = c * d * b\<^sup>2"
     1.9      unfolding power2_eq_square by (simp add: mult_ac)
    1.10 -  hence "0 < a * b * d\<twosuperior> \<longleftrightarrow> 0 < c * d * b\<twosuperior>"
    1.11 +  hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
    1.12      by simp
    1.13    thus "0 < a * b \<longleftrightarrow> 0 < c * d"
    1.14      using `b \<noteq> 0` and `d \<noteq> 0`