changeset 36334 | 068a01b4bc56 |
parent 36333 | 82356c9e218a |
child 36336 | 1c8fc1bae0b5 |
--- 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