author huffman Thu Feb 12 12:35:45 2009 -0800 (2009-02-12) changeset 29881 58f3c48dbbb7 parent 29880 3dee8ff45d3d child 29882 29154e67731d
fix document generation
```     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
1.23    by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf])
1.24
1.25 -text{* Matrix notation. NB: an MxN matrix is of type 'a^'n^'m, not 'a^'m^'n *}
1.26 +text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
1.27
1.28  consts generic_mult :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixr "\<star>" 75)
1.29
```