changed and retracted change of location of code lemmas.
authornipkow
Fri Mar 03 19:30:20 2006 +0100 (2006-03-03)
changeset 1917961ef97e3f531
parent 19178 9b295c37854f
child 19180 2b477ae4ece7
changed and retracted change of location of code lemmas.
src/HOL/Datatype.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Datatype.thy	Fri Mar 03 16:25:30 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Mar 03 19:30:20 2006 +0100
     1.3 @@ -229,24 +229,22 @@
     1.4    "(\<not> False) = True" by (rule HOL.simp_thms)
     1.5  
     1.6  lemma [code]:
     1.7 -  fixes x shows "(True \<and> True) = True"
     1.8 -  and "(False \<and> x) = False"
     1.9 -  and "(x \<and> False) = False" by simp_all
    1.10 +  shows "(False \<and> x) = False"
    1.11 +  and   "(True \<and> x) = x"
    1.12 +  and   "(x \<and> False) = False"
    1.13 +  and   "(x \<and> True) = x" by simp_all
    1.14  
    1.15  lemma [code]:
    1.16 -  fixes x shows "(False \<or> False) = False"
    1.17 -  and "(True \<or> x) = True"
    1.18 -  and "(x \<or> True) = True" by simp_all
    1.19 +  shows "(False \<or> x) = x"
    1.20 +  and   "(True \<or> x) = True"
    1.21 +  and   "(x \<or> False) = x"
    1.22 +  and   "(x \<or> True) = True" by simp_all
    1.23  
    1.24  declare
    1.25    if_True [code]
    1.26    if_False [code]
    1.27 -
    1.28 -lemma [code]:
    1.29 -  "fst (x, y) = x" by simp
    1.30 -
    1.31 -lemma [code]:
    1.32 -  "snd (x, y) = y" by simp
    1.33 +  fst_conv [code]
    1.34 +  snd_conv [code]
    1.35  
    1.36  code_generate True False Not "op &" "op |" If
    1.37  
     2.1 --- a/src/HOL/Product_Type.thy	Fri Mar 03 16:25:30 2006 +0100
     2.2 +++ b/src/HOL/Product_Type.thy	Fri Mar 03 19:30:20 2006 +0100
     2.3 @@ -776,8 +776,6 @@
     2.4  
     2.5  consts_code
     2.6    "Pair"    ("(_,/ _)")
     2.7 -  "fst"     ("fst")
     2.8 -  "snd"     ("snd")
     2.9  
    2.10  code_alias
    2.11    "*" "Product_Type.pair"