--- a/src/HOL/HOL.thy Fri Jul 07 09:28:39 2006 +0200
+++ b/src/HOL/HOL.thy Fri Jul 07 09:31:57 2006 +0200
@@ -1261,6 +1261,8 @@
in
+val evaluation_conv = evaluation_conv;
+
val eq_codegen_setup = Codegen.add_codegen "eq_codegen" eq_codegen;
val evaluation_oracle_setup =
@@ -1294,6 +1296,8 @@
in
+val normalization_conv = normalization_conv;
+
val normalization_oracle_setup =
Theory.add_oracle ("Normalization", normalization_oracle) #>
Method.add_method ("normalization", normalization_meth, "solve goal by normalization");