src/HOL/NthRoot.thy
changeset 53594 8a9fb53294f4
parent 53076 47c9aff07725
child 54413 88a036a95967
     1.1 --- a/src/HOL/NthRoot.thy	Thu Sep 12 09:03:52 2013 -0700
     1.2 +++ b/src/HOL/NthRoot.thy	Thu Sep 12 09:04:46 2013 -0700
     1.3 @@ -410,17 +410,17 @@
     1.4  lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
     1.5  unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
     1.6  
     1.7 -lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, simplified]
     1.8 -lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, simplified]
     1.9 -lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, simplified]
    1.10 -lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, simplified]
    1.11 -lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, simplified]
    1.12 +lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
    1.13 +lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
    1.14 +lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
    1.15 +lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, unfolded real_sqrt_zero]
    1.16 +lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, unfolded real_sqrt_zero]
    1.17  
    1.18 -lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, simplified]
    1.19 -lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, simplified]
    1.20 -lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, simplified]
    1.21 -lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, simplified]
    1.22 -lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified]
    1.23 +lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, unfolded real_sqrt_one]
    1.24 +lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, unfolded real_sqrt_one]
    1.25 +lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, unfolded real_sqrt_one]
    1.26 +lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, unfolded real_sqrt_one]
    1.27 +lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, unfolded real_sqrt_one]
    1.28  
    1.29  lemma isCont_real_sqrt: "isCont sqrt x"
    1.30  unfolding sqrt_def by (rule isCont_real_root)