src/HOL/Library/Euclidean_Space.thy
 changeset 29881 58f3c48dbbb7 parent 29844 4ac95212efcc child 29905 26ee9656872a
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu Feb 12 11:04:22 2009 -0800
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu Feb 12 12:35:45 2009 -0800
1.3 @@ -84,7 +84,7 @@
1.4  instance by (intro_classes)
1.5  end
1.6
1.7 -text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in real_vector *}
1.8 +text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
1.9
1.10  definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
1.11    where "c *s x = (\<chi> i. c * (x\$i))"
1.12 @@ -456,7 +456,7 @@
1.13      ultimately show ?thesis using alb by metis
1.14  qed
1.15
1.16 -text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case real ^1 *}
1.17 +text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case @{typ "real^1"} *}
1.18
1.19  lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
1.20  proof-
1.21 @@ -1737,7 +1737,7 @@
1.22    using u