| changeset 21404 | eb85850d3eb7 |
| parent 21331 | 1fd8ba48ae97 |
| child 21454 | a1937c51ed88 |
--- a/src/HOL/Product_Type.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Product_Type.thy Fri Nov 17 02:20:03 2006 +0100 @@ -110,7 +110,8 @@ Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" abbreviation - Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80) + Times :: "['a set, 'b set] => ('a * 'b) set" + (infixr "<*>" 80) where "A <*> B == Sigma A (%_. B)" notation (xsymbols)