--- 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