| changeset 42814 | 5af15f1e2ef6 |
| parent 41969 | 1cf3e4107a2a |
| child 43968 | 1fe23cfca01f |
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun May 15 17:45:53 2011 +0200 @@ -321,7 +321,7 @@ use "normarith.ML" method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) -*} "Proves simple linear statements about vector norms" +*} "prove simple linear statements about vector norms" text{* Hence more metric properties. *}