src/HOL/subset.ML
changeset 4159 4aff9b7e5597
parent 2893 2ee005e46d6d
child 5316 7a8975451a89
     1.1 --- a/src/HOL/subset.ML	Wed Nov 05 13:29:47 1997 +0100
     1.2 +++ b/src/HOL/subset.ML	Wed Nov 05 13:32:07 1997 +0100
     1.3 @@ -42,15 +42,6 @@
     1.4  by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
     1.5  qed "UN_least";
     1.6  
     1.7 -goal Set.thy "B(a) <= (UN x. B(x))";
     1.8 -by (REPEAT (ares_tac [UN1_I RS subsetI] 1));
     1.9 -qed "UN1_upper";
    1.10 -
    1.11 -val [prem] = goal Set.thy "[| !!x. B(x)<=C |] ==> (UN x. B(x)) <= C";
    1.12 -by (rtac subsetI 1);
    1.13 -by (REPEAT (eresolve_tac [asm_rl, UN1_E, prem RS subsetD] 1));
    1.14 -qed "UN1_least";
    1.15 -
    1.16  
    1.17  (*** Big Intersection -- greatest lower bound of a set ***)
    1.18  
    1.19 @@ -75,16 +66,6 @@
    1.20  by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
    1.21  qed "INT_greatest";
    1.22  
    1.23 -goal Set.thy "(INT x. B(x)) <= B(a)";
    1.24 -by (Blast_tac 1);
    1.25 -qed "INT1_lower";
    1.26 -
    1.27 -val [prem] = goal Set.thy
    1.28 -    "[| !!x. C<=B(x) |] ==> C <= (INT x. B(x))";
    1.29 -by (rtac (INT1_I RS subsetI) 1);
    1.30 -by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
    1.31 -qed "INT1_greatest";
    1.32 -
    1.33  (*** Finite Union -- the least upper bound of 2 sets ***)
    1.34  
    1.35  goal Set.thy "A <= A Un B";