src/HOL/Groebner_Basis.thy
changeset 57951 7896762b638b
parent 56850 13a7bca533a3
child 58777 6ba2f1fa243b
--- a/src/HOL/Groebner_Basis.thy	Sat Aug 16 14:12:39 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sat Aug 16 14:27:41 2014 +0200
@@ -33,16 +33,7 @@
     "\<not> P \<Longrightarrow> (P \<equiv> False)"
   by auto
 
-ML {*
-structure Algebra_Simplification = Named_Thms
-(
-  val name = @{binding algebra}
-  val description = "pre-simplification rules for algebraic methods"
-)
-*}
-
-setup Algebra_Simplification.setup
-
+named_theorems algebra "pre-simplification rules for algebraic methods"
 ML_file "Tools/groebner.ML"
 
 method_setup algebra = {*