updated to named_theorems;
authorwenzelm
Sat Aug 16 14:27:41 2014 +0200 (2014-08-16)
changeset 579517896762b638b
parent 57950 59c17b0b870d
child 57952 1a9a6dfc255f
updated to named_theorems;
src/HOL/Groebner_Basis.thy
src/HOL/Tools/groebner.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sat Aug 16 14:12:39 2014 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Aug 16 14:27:41 2014 +0200
     1.3 @@ -33,16 +33,7 @@
     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 -(
    1.10 -  val name = @{binding algebra}
    1.11 -  val description = "pre-simplification rules for algebraic methods"
    1.12 -)
    1.13 -*}
    1.14 -
    1.15 -setup Algebra_Simplification.setup
    1.16 -
    1.17 +named_theorems algebra "pre-simplification rules for algebraic methods"
    1.18  ML_file "Tools/groebner.ML"
    1.19  
    1.20  method_setup algebra = {*
     2.1 --- a/src/HOL/Tools/groebner.ML	Sat Aug 16 14:12:39 2014 +0200
     2.2 +++ b/src/HOL/Tools/groebner.ML	Sat Aug 16 14:27:41 2014 +0200
     2.3 @@ -924,7 +924,7 @@
     2.4  
     2.5  fun presimplify ctxt add_thms del_thms =
     2.6    asm_full_simp_tac (put_simpset HOL_basic_ss ctxt
     2.7 -    addsimps (Algebra_Simplification.get ctxt)
     2.8 +    addsimps (Named_Theorems.get ctxt @{named_theorems algebra})
     2.9      delsimps del_thms addsimps add_thms);
    2.10  
    2.11  fun ring_tac add_ths del_ths ctxt =