--- a/src/HOL/ex/CodeRevappl.thy Mon Sep 25 17:04:23 2006 +0200
+++ b/src/HOL/ex/CodeRevappl.thy Mon Sep 25 17:04:45 2006 +0200
@@ -10,6 +10,9 @@
section {* Combinators for structured results *}
+
+subsection {* primitive definitions *}
+
definition
revappl :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<triangleright>" 55)
revappl_def: "x \<triangleright> f = f x"
@@ -20,6 +23,9 @@
revappl_uncurry :: "'c \<times> 'a \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<turnstile>\<triangleright>" 55)
revappl_uncurry_split: "z \<turnstile>\<triangleright> f = f (fst z) (snd z)"
+
+subsection {* lemmas *}
+
lemma revappl_snd_def [code]:
"(y, x) |\<triangleright> f = (y, f x)" unfolding revappl_snd_split by simp