src/HOL/ex/Codegenerator.thy
changeset 21092 2e0a59d829d5
parent 21080 7d73aa966207
child 21125 9b7d35ca1eef
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Oct 23 11:05:07 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Oct 23 11:05:08 2006 +0200
     1.3 @@ -27,6 +27,8 @@
     1.4    "swap p = (let (x, y) = p in (y, x))"
     1.5    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
     1.6    "appl p = (let (f, x) = p in f x)"
     1.7 +  snd_three :: "'a * 'b * 'c => 'b"
     1.8 +  "snd_three a = id (\<lambda>(a, b, c). b) a"
     1.9  
    1.10  lemma [code]:
    1.11    "swap (x, y) = (y, x)"
    1.12 @@ -129,7 +131,7 @@
    1.13  code_gen
    1.14    "0::nat" "1::nat"
    1.15  code_gen
    1.16 -  Pair fst snd Let split swap
    1.17 +  Pair fst snd Let split swap snd_three
    1.18  code_gen
    1.19    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.20    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"