src/HOL/equalities.ML
changeset 5278 a903b66822e2
parent 5238 c449f23728df
child 5281 f4d16517b360
     1.1 --- a/src/HOL/equalities.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/equalities.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -85,8 +85,7 @@
     1.4  bind_thm ("insert_Collect", prove_goal thy 
     1.5  	"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
     1.6  
     1.7 -Goal
     1.8 -    "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
     1.9 +Goal "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
    1.10  by (Blast_tac 1);
    1.11  qed "UN_insert_distrib";
    1.12  
    1.13 @@ -305,8 +304,7 @@
    1.14  by (Blast_tac 1);
    1.15  qed "Un_Int_distrib2";
    1.16  
    1.17 -Goal
    1.18 - "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
    1.19 +Goal "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
    1.20  by (Blast_tac 1);
    1.21  qed "Un_Int_crazy";
    1.22  
    1.23 @@ -556,13 +554,11 @@
    1.24  by (Blast_tac 1);
    1.25  qed "Un_INT_distrib";
    1.26  
    1.27 -Goal
    1.28 -    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
    1.29 +Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
    1.30  by (Blast_tac 1);
    1.31  qed "Int_UN_distrib2";
    1.32  
    1.33 -Goal
    1.34 -    "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
    1.35 +Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
    1.36  by (Blast_tac 1);
    1.37  qed "Un_INT_distrib2";
    1.38