# HG changeset patch
# User haftmann
# Date 1252492146 -7200
# Node ID b4119bbb2b79ae63d2c83d8085b93c2100a48c92
# Parent  d68b7c1812114d8ba179e5a172dfc8eaa950d2ad# Parent  f3eab1682b0d434c948965ed5abe3f5188fc0b8b
merged

diff -r d68b7c181211 -r b4119bbb2b79 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Wed Sep 09 12:27:41 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy	Wed Sep 09 12:29:06 2009 +0200
@@ -4,17 +4,8 @@
 
 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]
@@ -137,5 +128,4 @@
 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