src/HOL/Prod.thy
changeset 8703 816d8f6513be
parent 6340 7d5cbd5819a0
child 9341 40bab6613000
     1.1 --- a/src/HOL/Prod.thy	Thu Apr 13 15:01:45 2000 +0200
     1.2 +++ b/src/HOL/Prod.thy	Thu Apr 13 15:01:50 2000 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    "_patterns"   :: [pttrn, patterns] => patterns ("_,/_")
     1.5  
     1.6    "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
     1.7 -  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
     1.8 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
     1.9  
    1.10  translations
    1.11    "(x, y, z)"    == "(x, (y, z))"
    1.12 @@ -68,7 +68,7 @@
    1.13       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
    1.14  
    1.15    "SIGMA x:A. B" => "Sigma A (%x. B)"
    1.16 -  "A Times B"    => "Sigma A (_K B)"
    1.17 +  "A <*> B"      => "Sigma A (_K B)"
    1.18  
    1.19  syntax (symbols)
    1.20    "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)