src/HOL/Prod.ML
changeset 5278 a903b66822e2
parent 5144 7ac22e5a05d7
child 5294 a84dd70e9925
     1.1 --- a/src/HOL/Prod.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Prod.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -253,8 +253,7 @@
     1.4  qed "prod_fun";
     1.5  Addsimps [prod_fun];
     1.6  
     1.7 -Goal 
     1.8 -    "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
     1.9 +Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
    1.10  by (rtac ext 1);
    1.11  by (pair_tac "x" 1);
    1.12  by (Asm_simp_tac 1);
    1.13 @@ -347,8 +346,7 @@
    1.14  Addsimps [Collect_split];
    1.15  
    1.16  (*Suggested by Pierre Chartier*)
    1.17 -Goal
    1.18 -     "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
    1.19 +Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
    1.20  by (Blast_tac 1);
    1.21  qed "UNION_Times_distrib";
    1.22