| changeset 6830 | f8aed3706af7 |
| parent 6394 | 3d9fd50fcc43 |
| child 7007 | b46ccfee8e59 |
--- a/src/HOL/Prod.ML Thu Jun 17 10:32:52 1999 +0200 +++ b/src/HOL/Prod.ML Thu Jun 17 10:33:33 1999 +0200 @@ -379,7 +379,7 @@ (*Suggested by Pierre Chartier*) Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)"; by (Blast_tac 1); -qed "UNION_Times_distrib"; +qed "UN_Times_distrib"; Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"; by (Fast_tac 1);