--- a/src/HOL/ex/Normalization_by_Evaluation.thy Mon Dec 06 14:17:35 2010 -0800
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Tue Dec 07 09:36:12 2010 +0100
@@ -66,7 +66,7 @@
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
- by normalization
+ by normalization rule
lemma "rev [a, b, c] = [c, b, a]" by normalization
value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"