# HG changeset patch
# User haftmann
# Date 1222771757 -7200
# Node ID bfa368164502d3dd57159186cda4df789b8864c0
# Parent  05d202350b8d0ff1d7af59edaa4444ed57a076a6
tuned

diff -r 05d202350b8d -r bfa368164502 src/HOL/ex/NormalForm.thy
--- 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