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
```