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