src/HOL/Product_Type.thy
changeset 22838 466599ecf610
parent 22744 5cbe966d67a2
child 22886 cdff6ef76009
     1.1 --- a/src/HOL/Product_Type.thy	Sun May 06 18:07:06 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sun May 06 21:49:23 2007 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  global
     1.5  
     1.6  typedef (Prod)
     1.7 -  ('a, 'b) "*"    (infixr 20)
     1.8 +  ('a, 'b) "*"    (infixr "*" 20)
     1.9      = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.10  proof
    1.11    fix a b show "Pair_Rep a b : ?Prod"