--- a/src/HOL/Univ.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Univ.ML Thu Apr 13 15:01:50 2000 +0200
@@ -582,7 +582,7 @@
(*** Bounding theorems ***)
-Goal "(dprod (A Times B) (C Times D)) <= (uprod A C) Times (uprod B D)";
+Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
by (Blast_tac 1);
qed "dprod_Sigma";
@@ -595,7 +595,7 @@
by (Blast_tac 1);
qed "dprod_subset_Sigma2";
-Goal "(dsum (A Times B) (C Times D)) <= (usum A C) Times (usum B D)";
+Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
by (Blast_tac 1);
qed "dsum_Sigma";