equal
deleted
inserted
replaced
319 using norm_ge_zero[of "x - y"] by auto |
319 using norm_ge_zero[of "x - y"] by auto |
320 |
320 |
321 use "normarith.ML" |
321 use "normarith.ML" |
322 |
322 |
323 method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
323 method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
324 *} "Proves simple linear statements about vector norms" |
324 *} "prove simple linear statements about vector norms" |
325 |
325 |
326 |
326 |
327 text{* Hence more metric properties. *} |
327 text{* Hence more metric properties. *} |
328 |
328 |
329 lemma norm_triangle_half_r: |
329 lemma norm_triangle_half_r: |