# HG changeset patch
# User haftmann
# Date 1172846600 -3600
# Node ID bdf16741d0398c86c9fbf6353911aaecd20968ce
# Parent  14098da702e05f7f2b2d1f799b2c04be6729b3f8
using "fst" "snd" for Haskell code

diff -r 14098da702e0 -r bdf16741d039 src/HOL/Product_Type.thy
--- 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) {*