# HG changeset patch
# User nipkow
# Date 1152257517 -7200
# Node ID fa655d0e18c23ed9af2bae43cb805e25cc2c0b43
# Parent  80c79876d2de7443d1118c8fe6581e9cd33cd033
made evaluation_conv and normalization_conv visible.

diff -r 80c79876d2de -r fa655d0e18c2 src/HOL/HOL.thy
--- 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");