--- a/src/HOL/ex/NormalForm.thy Tue Sep 23 18:11:43 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy Tue Sep 23 18:11:44 2008 +0200
@@ -91,8 +91,7 @@
lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
lemma "last [a, b, c] = c" by normalization rule
-lemma "last ([a, b, c] @ xs) = (if null xs then c else last xs)"
- by normalization rule
+lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization rule
lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization rule
lemma "(-4::int) * 2 = -8" by normalization