# HG changeset patch
# User paulson
# Date 835968509 -7200
# Node ID 8e5e2fef6d269378389faa982f7fc2f4a9ab3867
# Parent  149b2e69633e5a36aecc75323a5114d0c3fee813
Added contra_subsetD and rev_contra_subsetD

diff -r 149b2e69633e -r 8e5e2fef6d26 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Jun 28 15:27:53 1996 +0200
+++ b/src/HOL/Set.ML	Fri Jun 28 15:28:29 1996 +0200
@@ -110,6 +110,12 @@
 qed_goal "rev_subsetD" Set.thy "[| c:A;  A <= B |] ==> c:B"
  (fn prems=>  [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]);
 
+qed_goal "contra_subsetD" Set.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
+ (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
+
+qed_goal "rev_contra_subsetD" Set.thy "!!c. [| c ~: B;  A <= B |] ==> c ~: A"
+ (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
+
 (*Classical elimination rule*)
 val major::prems = goalw Set.thy [subset_def] 
     "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";