src/HOL/Univ.ML
changeset 8703 816d8f6513be
parent 8292 93e125b21220
child 8709 483a3eb96c7e
--- 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";