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