# HG changeset patch
# User paulson
# Date 971771167 -7200
# Node ID 08083bd2a64d99759543572ef1d898851c1e3de7
# Parent  529c65b5dcde7dfb44bcef3a310cd71f8582a960
tidying; removed unused rev_contra_subsetD

diff -r 529c65b5dcde -r 08083bd2a64d src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Oct 17 10:23:16 2000 +0200
+++ b/src/HOL/Set.ML	Tue Oct 17 10:26:07 2000 +0200
@@ -152,14 +152,6 @@
 (*Converts A<=B to x:A ==> x:B*)
 fun impOfSubs th = th RSN (2, rev_subsetD);
 
-Goal "[| A <= B; c ~: B |] ==> c ~: A";
-by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
-qed "contra_subsetD";
-
-Goal "[| c ~: B;  A <= B |] ==> c ~: A";
-by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
-qed "rev_contra_subsetD";
-
 (*Classical elimination rule*)
 val major::prems = Goalw [subset_def] 
     "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
@@ -173,9 +165,13 @@
 AddSIs [subsetI];
 AddEs  [subsetD, subsetCE];
 
+Goal "[| A <= B; c ~: B |] ==> c ~: A";
+by (Blast_tac 1);
+qed "contra_subsetD";
+
 Goal "A <= (A::'a set)";
 by (Fast_tac 1);
-qed "subset_refl";		(*Blast_tac would try order_refl and fail*)
+qed "subset_refl";
 
 Goal "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
 by (Blast_tac 1);