# HG changeset patch
# User haftmann
# Date 1252491862 -7200
# Node ID f3eab1682b0d434c948965ed5abe3f5188fc0b8b
# Parent  e129333b9df05f75069e165623930c7885212ef2
dropped accidental code additions

diff -r e129333b9df0 -r f3eab1682b0d src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Wed Sep 09 11:31:20 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy	Wed Sep 09 12:24:22 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