src/HOL/Real_Vector_Spaces.thy
changeset 54863 82acc20ded73
parent 54785 4876fb408c0d
child 54890 cb892d835803
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -1097,12 +1097,12 @@
     1.4    show ?thesis
     1.5    proof (intro exI impI conjI allI)
     1.6      show "0 < max 1 K"
     1.7 -      by (rule order_less_le_trans [OF zero_less_one le_maxI1])
     1.8 +      by (rule order_less_le_trans [OF zero_less_one max.cobounded1])
     1.9    next
    1.10      fix x
    1.11      have "norm (f x) \<le> norm x * K" using K .
    1.12      also have "\<dots> \<le> norm x * max 1 K"
    1.13 -      by (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
    1.14 +      by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero])
    1.15      finally show "norm (f x) \<le> norm x * max 1 K" .
    1.16    qed
    1.17  qed
    1.18 @@ -1138,9 +1138,9 @@
    1.19    "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
    1.20  apply (cut_tac bounded, erule exE)
    1.21  apply (rule_tac x="max 1 K" in exI, safe)
    1.22 -apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
    1.23 +apply (rule order_less_le_trans [OF zero_less_one max.cobounded1])
    1.24  apply (drule spec, drule spec, erule order_trans)
    1.25 -apply (rule mult_left_mono [OF le_maxI2])
    1.26 +apply (rule mult_left_mono [OF max.cobounded2])
    1.27  apply (intro mult_nonneg_nonneg norm_ge_zero)
    1.28  done
    1.29