src/HOL/Analysis/Linear_Algebra.thy
changeset 64122 74fde524799e
parent 63938 f6ce08859d4c
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Oct 09 16:27:01 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Oct 10 15:45:41 2016 +0100
     1.3 @@ -2178,7 +2178,7 @@
     1.4  
     1.5  text \<open>More lemmas about dimension.\<close>
     1.6  
     1.7 -lemma dim_UNIV: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
     1.8 +lemma dim_UNIV [simp]: "dim (UNIV :: 'a::euclidean_space set) = DIM('a)"
     1.9    using independent_Basis
    1.10    by (intro dim_unique[of Basis]) auto
    1.11