# HG changeset patch
# User haftmann
# Date 1161594308 -7200
# Node ID 2e0a59d829d5f67b7db8b8f6f131be34e44ef7da
# Parent  5061e3e56484f775c9200aeed44ddc5566b7255b
added example with split

diff -r 5061e3e56484 -r 2e0a59d829d5 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Oct 23 11:05:07 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Oct 23 11:05:08 2006 +0200
@@ -27,6 +27,8 @@
   "swap p = (let (x, y) = p in (y, x))"
   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
   "appl p = (let (f, x) = p in f x)"
+  snd_three :: "'a * 'b * 'c => 'b"
+  "snd_three a = id (\<lambda>(a, b, c). b) a"
 
 lemma [code]:
   "swap (x, y) = (y, x)"
@@ -129,7 +131,7 @@
 code_gen
   "0::nat" "1::nat"
 code_gen
-  Pair fst snd Let split swap
+  Pair fst snd Let split swap snd_three
 code_gen
   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"