--- a/src/HOL/HOL.thy Fri Feb 25 12:16:18 2011 +0100
+++ b/src/HOL/HOL.thy Mon Feb 28 15:06:36 2011 +0000
@@ -908,6 +908,8 @@
declare ex_ex1I [rule del, intro! 2]
and ex1I [intro]
+declare ext [intro]
+
lemmas [intro?] = ext
and [elim?] = ex1_implies_ex