diff -r 91614f0eb250 -r ac7b7003f177 simpdata.ML
--- a/simpdata.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/simpdata.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -52,6 +52,7 @@
 val simp_thms = map prover
  [ "(x=x) = True",
    "(~True) = False", "(~False) = True", "(~ ~ P) = P",
+   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    "(True=P) = P", "(P=True) = P",
    "(True --> P) = P", "(False --> P) = True", 
    "(P --> True) = True", "(P --> P) = True",
@@ -101,6 +102,17 @@
 fun split_tac splits =
   mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);
 
+(* eliminiation of existential quantifiers in assumptions *)
+
+val ex_all_equiv =
+  let val lemma1 = prove_goal HOL.thy
+        "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
+        (fn prems => [resolve_tac prems 1, etac exI 1]);
+      val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+        "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
+        (fn prems => [REPEAT(resolve_tac prems 1)])
+  in equal_intr lemma1 lemma2 end;
+
 (** '&' congruence rule: not included by default! *)
 
 val conj_cong = impI RSN