src/HOL/Real/HahnBanach/Subspace.thy
changeset 8169 77b3bc101de5
parent 7978 1b99ee57d131
child 8203 2fcc6017cb72
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Jan 28 21:57:15 2000 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Jan 28 21:58:39 2000 +0100
     1.3 @@ -391,10 +391,13 @@
     1.4         qed;
     1.5        qed;
     1.6        show "{<0>} <= H Int lin x0";
     1.7 -      proof (intro subsetI, elim singletonE, intro IntI, 
     1.8 -        (simp only:)+);
     1.9 -        show "<0>:H"; ..;
    1.10 -        from lin_vs; show "<0> : lin x0"; ..;
    1.11 +      proof -;
    1.12 +	have "<0>: H Int lin x0";
    1.13 +	proof (rule IntI);
    1.14 +	  show "<0>:H"; ..;
    1.15 +	  from lin_vs; show "<0> : lin x0"; ..;
    1.16 +	qed;
    1.17 +	thus ?thesis; by simp;
    1.18        qed;
    1.19      qed;
    1.20      show "is_subspace (lin x0) E"; ..;