src/HOL/Groebner_Basis.thy

--- a/src/HOL/Groebner_Basis.thy	Thu May 06 16:32:21 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy	Thu May 06 16:40:02 2010 +0200
@@ -412,6 +412,15 @@
     "\<not> P \<Longrightarrow> (P \<equiv> False)"
   by auto
 
+ML {*
+structure Algebra_Simplification = Named_Thms(
+  val name = "algebra"
+  val description = "pre-simplification rules for algebraic methods"
+)
+*}
+
+setup Algebra_Simplification.setup
+
 use "Tools/Groebner_Basis/groebner.ML"
 
 method_setup algebra =