--- 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