src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Mon Feb 20 11:37:18 2006 +0100
+++ b/src/HOL/Datatype.thy	Mon Feb 20 11:38:06 2006 +0100
@@ -235,6 +235,12 @@
     ml (target_atom "(__,/ __)")
     haskell (target_atom "(__,/ __)")
 
+lemma [code]:
+  "fst (x, y) = x" by simp
+
+lemma [code]:
+  "snd (x, y) = y" by simp
+
 code_syntax_const
   1 :: "nat"
     ml ("{*Suc 0*}")