diff -r 62e6c9b67c6f -r e129333b9df0 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Tue Sep 08 18:31:26 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy	Wed Sep 09 11:31:20 2009 +0200
@@ -4,8 +4,17 @@
 
 theory NormalForm
 imports Main Rational
+uses "~~/src/Tools/nbe.ML"
 begin
 
+setup {*
+  Nbe.add_const_alias @{thm equals_alias_cert}
+*}
+
+method_setup normalization = {*
+  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
+*} "solve goal by normalization"
+
 lemma "True" by normalization
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
@@ -120,4 +129,13 @@
 normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
 normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
 
+(* handling of type classes in connection with equality *)
+
+lemma "map f [x, y] = [f x, f y]" by normalization
+lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
+lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
+lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
+lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
+
+
 end