src/HOL/Product_Type.thy
changeset 22389 bdf16741d039
parent 22349 a4e82dd93202
child 22439 b709739c69e6
     1.1 --- a/src/HOL/Product_Type.thy	Fri Mar 02 15:43:19 2007 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Mar 02 15:43:20 2007 +0100
     1.3 @@ -823,6 +823,9 @@
     1.4    (OCaml "!((_),/ (_))")
     1.5    (Haskell "!((_),/ (_))")
     1.6  
     1.7 +code_const fst and snd
     1.8 +  (Haskell "fst" and "snd")
     1.9 +
    1.10  types_code
    1.11    "*"     ("(_ */ _)")
    1.12  attach (term_of) {*