src/HOL/Product_Type.thy
changeset 19008 14c1b2f5dda4
parent 18963 3adfc9dfb30a
child 19039 8eae46249628
     1.1 --- a/src/HOL/Product_Type.thy	Fri Feb 10 02:22:59 2006 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 10 09:09:07 2006 +0100
     1.3 @@ -780,7 +780,7 @@
     1.4    "snd"     ("snd")
     1.5  
     1.6  code_alias
     1.7 -  "*" "Product_Type.*"
     1.8 +  "*" "Product_Type.pair"
     1.9    "Pair" "Product_Type.Pair"
    1.10    "fst" "Product_Type.fst"
    1.11    "snd" "Product_Type.snd"