src/HOL/HOL.thy
changeset 13723 c7d104550205
parent 13638 2b234b079245
child 13763 f94b569cd610
--- a/src/HOL/HOL.thy	Wed Nov 20 10:43:20 2002 +0100
+++ b/src/HOL/HOL.thy	Thu Nov 21 17:40:11 2002 +0100
@@ -512,6 +512,9 @@
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
 
+lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
+by blast+
+
 theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
   apply (rule iffI)
   apply (rule_tac a = "%x. THE y. P x y" in ex1I)