src/HOL/Datatype.thy
changeset 19111 1f6112de1d0f
parent 18757 f0d901bc0686
child 19138 42ff710d432f
     1.1 --- a/src/HOL/Datatype.thy	Mon Feb 20 11:37:18 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Feb 20 11:38:06 2006 +0100
     1.3 @@ -235,6 +235,12 @@
     1.4      ml (target_atom "(__,/ __)")
     1.5      haskell (target_atom "(__,/ __)")
     1.6  
     1.7 +lemma [code]:
     1.8 +  "fst (x, y) = x" by simp
     1.9 +
    1.10 +lemma [code]:
    1.11 +  "snd (x, y) = y" by simp
    1.12 +
    1.13  code_syntax_const
    1.14    1 :: "nat"
    1.15      ml ("{*Suc 0*}")