# HG changeset patch
# User haftmann
# Date 1167915697 -3600
# Node ID 29d5cdd1cc03984b7846db361abc09e0217876c9
# Parent  76d3d258cfa366bc5797b1dd7ddbd6567b984c39
more term examples

diff -r 76d3d258cfa3 -r 29d5cdd1cc03 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Thu Jan 04 11:56:53 2007 +0100
+++ b/src/HOL/ex/NormalForm.thy	Thu Jan 04 14:01:37 2007 +0100
@@ -112,4 +112,10 @@
 
 normal_form "Suc 0 \<in> set ms"
 
+normal_form "f"
+normal_form "f x"
+normal_form "(f o g) x"
+normal_form "(f o id) x"
+normal_form "\<lambda>x. x"
+
 end