# HG changeset patch
# User wenzelm
# Date 949093119 -3600
# Node ID 77b3bc101de51068b26937e5d786a1da97d04dcc
# Parent  9d2ac5439089509b924fae6f3dca060902acc8e8
eliminated proof script;

diff -r 9d2ac5439089 -r 77b3bc101de5 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Jan 28 21:57:15 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Jan 28 21:58:39 2000 +0100
@@ -391,10 +391,13 @@
        qed;
       qed;
       show "{<0>} <= H Int lin x0";
-      proof (intro subsetI, elim singletonE, intro IntI, 
-        (simp only:)+);
-        show "<0>:H"; ..;
-        from lin_vs; show "<0> : lin x0"; ..;
+      proof -;
+	have "<0>: H Int lin x0";
+	proof (rule IntI);
+	  show "<0>:H"; ..;
+	  from lin_vs; show "<0> : lin x0"; ..;
+	qed;
+	thus ?thesis; by simp;
       qed;
     qed;
     show "is_subspace (lin x0) E"; ..;