tidying; removed unused rev_contra_subsetD
authorpaulson
Tue Oct 17 10:26:07 2000 +0200 (2000-10-17)
changeset 1023308083bd2a64d
parent 10232 529c65b5dcde
child 10234 c8726d4ee89a
tidying; removed unused rev_contra_subsetD
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Tue Oct 17 10:23:16 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Tue Oct 17 10:26:07 2000 +0200
     1.3 @@ -152,14 +152,6 @@
     1.4  (*Converts A<=B to x:A ==> x:B*)
     1.5  fun impOfSubs th = th RSN (2, rev_subsetD);
     1.6  
     1.7 -Goal "[| A <= B; c ~: B |] ==> c ~: A";
     1.8 -by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
     1.9 -qed "contra_subsetD";
    1.10 -
    1.11 -Goal "[| c ~: B;  A <= B |] ==> c ~: A";
    1.12 -by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
    1.13 -qed "rev_contra_subsetD";
    1.14 -
    1.15  (*Classical elimination rule*)
    1.16  val major::prems = Goalw [subset_def] 
    1.17      "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
    1.18 @@ -173,9 +165,13 @@
    1.19  AddSIs [subsetI];
    1.20  AddEs  [subsetD, subsetCE];
    1.21  
    1.22 +Goal "[| A <= B; c ~: B |] ==> c ~: A";
    1.23 +by (Blast_tac 1);
    1.24 +qed "contra_subsetD";
    1.25 +
    1.26  Goal "A <= (A::'a set)";
    1.27  by (Fast_tac 1);
    1.28 -qed "subset_refl";		(*Blast_tac would try order_refl and fail*)
    1.29 +qed "subset_refl";
    1.30  
    1.31  Goal "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
    1.32  by (Blast_tac 1);