src/HOL/Groebner_Basis.thy
changeset 36702 b455ebd63799
parent 36700 9b85b9d74b83
child 36712 2f4c318861b3
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu May 06 16:32:21 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu May 06 16:40:02 2010 +0200
     1.3 @@ -412,6 +412,15 @@
     1.4      "\<not> P \<Longrightarrow> (P \<equiv> False)"
     1.5    by auto
     1.6  
     1.7 +ML {*
     1.8 +structure Algebra_Simplification = Named_Thms(
     1.9 +  val name = "algebra"
    1.10 +  val description = "pre-simplification rules for algebraic methods"
    1.11 +)
    1.12 +*}
    1.13 +
    1.14 +setup Algebra_Simplification.setup
    1.15 +
    1.16  use "Tools/Groebner_Basis/groebner.ML"
    1.17  
    1.18  method_setup algebra =