src/HOL/ex/NormalForm.thy
changeset 21987 29d5cdd1cc03
parent 21460 cda5cd8bfd16
child 22394 54ea68b5a92f
--- 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