src/HOL/Real/HahnBanach/Subspace.thy
changeset 9969 4753185f1dd2
parent 9941 fe05af7ec816
child 10309 a7f961fb62c6
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 15 11:34:46 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 15 12:39:57 2000 +0200
     1.3 @@ -469,7 +469,7 @@
     1.4      qed
     1.5    qed
     1.6    hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
     1.7 -    by (rule select1_equality) (force!)
     1.8 +    by (rule some1_equality) (force!)
     1.9    thus "h' x = h y + a * xi" by (simp! add: Let_def)
    1.10  qed
    1.11