# HG changeset patch
# User nipkow
# Date 1141410620 -3600
# Node ID 61ef97e3f531a962a4548e3e6f36b378552a73c2
# Parent  9b295c37854fd2cb3610e5732748ccf1cc2cc557
changed and retracted change of location of code lemmas.

diff -r 9b295c37854f -r 61ef97e3f531 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Mar 03 16:25:30 2006 +0100
+++ b/src/HOL/Datatype.thy	Fri Mar 03 19:30:20 2006 +0100
@@ -229,24 +229,22 @@
   "(\<not> False) = True" by (rule HOL.simp_thms)
 
 lemma [code]:
-  fixes x shows "(True \<and> True) = True"
-  and "(False \<and> x) = False"
-  and "(x \<and> False) = False" by simp_all
+  shows "(False \<and> x) = False"
+  and   "(True \<and> x) = x"
+  and   "(x \<and> False) = False"
+  and   "(x \<and> True) = x" by simp_all
 
 lemma [code]:
-  fixes x shows "(False \<or> False) = False"
-  and "(True \<or> x) = True"
-  and "(x \<or> True) = True" by simp_all
+  shows "(False \<or> x) = x"
+  and   "(True \<or> x) = True"
+  and   "(x \<or> False) = x"
+  and   "(x \<or> True) = True" by simp_all
 
 declare
   if_True [code]
   if_False [code]
-
-lemma [code]:
-  "fst (x, y) = x" by simp
-
-lemma [code]:
-  "snd (x, y) = y" by simp
+  fst_conv [code]
+  snd_conv [code]
 
 code_generate True False Not "op &" "op |" If
 
diff -r 9b295c37854f -r 61ef97e3f531 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Mar 03 16:25:30 2006 +0100
+++ b/src/HOL/Product_Type.thy	Fri Mar 03 19:30:20 2006 +0100
@@ -776,8 +776,6 @@
 
 consts_code
   "Pair"    ("(_,/ _)")
-  "fst"     ("fst")
-  "snd"     ("snd")
 
 code_alias
   "*" "Product_Type.pair"