--- a/src/HOL/ex/NormalForm.thy Tue Sep 30 12:49:16 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy Tue Sep 30 12:49:17 2008 +0200
@@ -71,7 +71,8 @@
lemma "[] @ xs = xs" by normalization
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 rule+
+lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
+ by normalization rule+
lemma "rev [a, b, c] = [c, b, a]" by normalization
normal_form "rev (a#b#cs) = rev cs @ [b, a]"
normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
@@ -95,9 +96,6 @@
lemma "last [a, b, c] = c" by normalization
lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization
-lemma [code nbe]:
- "eq_class.eq (x :: int) x \<longleftrightarrow> True" unfolding eq by rule+
-
lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
lemma "(-4::int) * 2 = -8" by normalization
lemma "abs ((-4::int) + 2 * 1) = 2" by normalization