# HG changeset patch
# User nipkow
# Date 1181891346 -7200
# Node ID 6d72ababc58fe76179633a061c07c7863b84d624
# Parent  15fb6637690ea0a5bda339d9f8be703566e57141
Church numerals added

diff -r 15fb6637690e -r 6d72ababc58f src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Thu Jun 14 23:04:40 2007 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Jun 15 09:09:06 2007 +0200
@@ -116,4 +116,10 @@
 normal_form "(f o id) x"
 normal_form "\<lambda>x. x"
 
+(* Church numerals: *)
+
+normal_form "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+
 end