equal
deleted
inserted
replaced
129 mult_1_left |
129 mult_1_left |
130 mult_1_right |
130 mult_1_right |
131 |
131 |
132 ML_file "normarith.ML" |
132 ML_file "normarith.ML" |
133 |
133 |
134 method_setup norm = \<open> |
134 method_setup%important norm = \<open> |
135 Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
135 Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
136 \<close> "prove simple linear statements about vector norms" |
136 \<close> "prove simple linear statements about vector norms" |
137 |
137 |
138 |
138 |
139 text \<open>Hence more metric properties.\<close> |
139 text \<open>Hence more metric properties.\<close> |
140 |
140 |
141 lemma dist_triangle_add: |
141 lemma%important dist_triangle_add: |
142 fixes x y x' y' :: "'a::real_normed_vector" |
142 fixes x y x' y' :: "'a::real_normed_vector" |
143 shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'" |
143 shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'" |
144 by norm |
144 by norm |
145 |
145 |
146 lemma dist_triangle_add_half: |
146 lemma dist_triangle_add_half: |