# HG changeset patch
# User wenzelm
# Date 1137351531 -3600
# Node ID a50587cd8414b881a5b86061adf519fa49f6535b
# Parent  abf0f018b5ece7f68b890bc8b091112d5bce9f7d
prefer ex1I over ex_ex1I in single-step reasoning;

diff -r abf0f018b5ec -r a50587cd8414 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jan 14 22:25:34 2006 +0100
+++ b/src/HOL/HOL.thy	Sun Jan 15 19:58:51 2006 +0100
@@ -918,6 +918,9 @@
 setup Classical.setup
 setup clasetup
 
+declare ex_ex1I [rule del, intro! 2]
+  and ex1I [intro]
+
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
 
diff -r abf0f018b5ec -r a50587cd8414 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sat Jan 14 22:25:34 2006 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jan 15 19:58:51 2006 +0100
@@ -435,7 +435,7 @@
 proof -
   from x y x' have "x \<in> H + lin x'" by auto
   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
-  proof
+  proof (rule ex_ex1I)
     from x y show "\<exists>p. ?P p" by blast
     fix p q assume p: "?P p" and q: "?P q"
     show "p = q"
@@ -450,7 +450,6 @@
         from xq show "fst q \<in> H" ..
         from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
           by simp
-        apply_end assumption+
       qed
       thus ?thesis by (cases p, cases q) simp
     qed