src/HOL/Multivariate_Analysis/Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Apr 24 13:31:52 2010 -0700
@@ -114,7 +114,7 @@
   instance by (intro_classes)
 end
 
-text{* The ordering on real^1 is linear. *}
+text{* The ordering on @{typ "real^1"} is linear. *}
 
 class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
 begin