src/HOL/Real/HahnBanach/Subspace.thy
changeset 9370 cccba6147dae
parent 9035 371f023d3dbd
child 9374 153853af318b
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 16 20:57:34 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jul 16 20:59:06 2000 +0200
     1.3 @@ -420,7 +420,7 @@
     1.4    "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
     1.5    x0 ~= 00 |] 
     1.6    ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"
     1.7 -proof (rule, unfold split_paired_all)
     1.8 +proof (rule, unfold split_tupled_all)
     1.9    assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
    1.10      "x0 ~= 00"
    1.11    have h: "is_vectorspace H" ..
    1.12 @@ -459,7 +459,7 @@
    1.13      show "xa = ya" 
    1.14      proof -
    1.15        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" 
    1.16 -        by (rule Pair_fst_snd_eq [RS iffD2])
    1.17 +        by (simp add: Pair_fst_snd_eq)
    1.18        have x: "x = fst xa + snd xa (*) x0 & fst xa : H" 
    1.19          by (force!)
    1.20        have y: "x = fst ya + snd ya (*) x0 & fst ya : H"