# HG changeset patch
# User haftmann
# Date 1159196685 -7200
# Node ID eb0193afca14119867e32f7f1f6765cc4562ede1
# Parent  f77bd47a70df3e61cb263453f09a8562714856e9
inserted headings

diff -r f77bd47a70df -r eb0193afca14 src/HOL/ex/CodeRevappl.thy
--- 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