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