# HG changeset patch
# User paulson
# Date 838376792 -7200
# Node ID 661603db8ee2dcfb4bd68ab2bf2311ea45c6f7af
# Parent  acb7363994cb0abf6d3c234e0348ee33b684f028
Addition of contra_subsetD and rev_contra_subsetD

diff -r acb7363994cb -r 661603db8ee2 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Fri Jul 26 12:25:15 1996 +0200
+++ b/src/ZF/ZF.ML	Fri Jul 26 12:26:32 1996 +0200
@@ -111,6 +111,12 @@
 qed_goal "rev_subsetD" ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
  (fn _=> [REPEAT (ares_tac [subsetD] 1)]);
 
+qed_goal "contra_subsetD" ZF.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
+ (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
+
+qed_goal "rev_contra_subsetD" ZF.thy "!!c. [| c ~: B;  A <= B |] ==> c ~: A"
+ (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
+
 qed_goal "subset_refl" ZF.thy "A <= A"
  (fn _=> [ (rtac subsetI 1), atac 1 ]);