author | paulson |
Thu, 17 Jun 1999 10:33:33 +0200 | |
changeset 6830 | f8aed3706af7 |
parent 6829 | 50459a995aa3 |
child 6831 | 799859f2e657 |
src/HOL/Prod.ML | file | annotate | diff | comparison | revisions |
--- 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);