using "fst" "snd" for Haskell code
authorhaftmann
Fri, 02 Mar 2007 15:43:20 +0100
changeset 22389 bdf16741d039
parent 22388 14098da702e0
child 22390 378f34b1e380
using "fst" "snd" for Haskell code
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) {*