# HG changeset patch
# User huffman
# Date 1234470945 28800
# Node ID 58f3c48dbbb7dcbb61c88846361701f8898447a5
# Parent  3dee8ff45d3d0e0b6c1d16b5f58bbb5c40bad8a6
fix document generation

diff -r 3dee8ff45d3d -r 58f3c48dbbb7 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Thu Feb 12 11:04:22 2009 -0800
+++ b/src/HOL/Library/Euclidean_Space.thy	Thu Feb 12 12:35:45 2009 -0800
@@ -84,7 +84,7 @@
 instance by (intro_classes)
 end
 
-text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in real_vector *}
+text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
 
 definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
   where "c *s x = (\<chi> i. c * (x$i))"
@@ -456,7 +456,7 @@
     ultimately show ?thesis using alb by metis
 qed
 
-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 *}
+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"} *}
 
 lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
 proof-
@@ -1737,7 +1737,7 @@
   using u
   by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf])
 
-text{* Matrix notation. NB: an MxN matrix is of type 'a^'n^'m, not 'a^'m^'n *}
+text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
 
 consts generic_mult :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixr "\<star>" 75)