src/HOL/equalities.ML
changeset 2512 0231e4f467f2
parent 2031 03a843f0f447
child 2513 d708d8cdc8e8
     1.1 --- a/src/HOL/equalities.ML	Fri Jan 17 10:04:28 1997 +0100
     1.2 +++ b/src/HOL/equalities.ML	Fri Jan 17 10:09:46 1997 +0100
     1.3 @@ -455,6 +455,18 @@
     1.4  by (Fast_tac 1);
     1.5  qed "Un_INT_distrib2";
     1.6  
     1.7 +
     1.8 +section"Bounded quantifiers";
     1.9 +
    1.10 +goal Set.thy "(!x:insert a A.P x) = (P a & (!x:A.P x))";
    1.11 +by (Fast_tac 1);
    1.12 +qed "Ball_insert";
    1.13 +
    1.14 +goal Set.thy "(!x:A Un B.P x) = ((!x:A.P x) & (!x:B.P x))";
    1.15 +by (Fast_tac 1);
    1.16 +qed "Ball_Un";
    1.17 +
    1.18 +
    1.19  section "-";
    1.20  
    1.21  goal Set.thy "A-A = {}";