fix document generation
authorhuffman
Thu Feb 12 12:35:45 2009 -0800 (2009-02-12)
changeset 2988158f3c48dbbb7
parent 29880 3dee8ff45d3d
child 29882 29154e67731d
fix document generation
src/HOL/Library/Euclidean_Space.thy
     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