| changeset 20380 | 14f9f2a1caa6 |
| parent 20105 | 454f4be984b7 |
| child 20415 | e3d2d7b01279 |
--- a/src/HOL/Product_Type.thy Mon Aug 14 13:46:05 2006 +0200 +++ b/src/HOL/Product_Type.thy Mon Aug 14 13:46:06 2006 +0200 @@ -772,12 +772,6 @@ consts_code "Pair" ("(_,/ _)") -code_alias - "*" "Product_Type.pair" - "Pair" "Product_Type.Pair" - "fst" "Product_Type.fst" - "snd" "Product_Type.snd" - ML {* fun strip_abs_split 0 t = ([], t)