# HG changeset patch # User wenzelm # Date 1408192061 -7200 # Node ID 7896762b638be63489dedfba34a6705f9a4711b6 # Parent 59c17b0b870d3b45cb4d85a02f17e552f9ebb479 updated to named_theorems; diff -r 59c17b0b870d -r 7896762b638b src/HOL/Groebner_Basis.thy --- 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 @@ "\ P \ (P \ 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 = {* diff -r 59c17b0b870d -r 7896762b638b src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Sat Aug 16 14:12:39 2014 +0200 +++ b/src/HOL/Tools/groebner.ML Sat Aug 16 14:27:41 2014 +0200 @@ -924,7 +924,7 @@ fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt - addsimps (Algebra_Simplification.get ctxt) + addsimps (Named_Theorems.get ctxt @{named_theorems algebra}) delsimps del_thms addsimps add_thms); fun ring_tac add_ths del_ths ctxt =