src/HOL/Groebner_Basis.thy
changeset 45294 3c5d3d286055
parent 36752 cf558aeb35b0
child 47142 d64fa2ca54b8
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -32,8 +32,9 @@
     1.4    by auto
     1.5  
     1.6  ML {*
     1.7 -structure Algebra_Simplification = Named_Thms(
     1.8 -  val name = "algebra"
     1.9 +structure Algebra_Simplification = Named_Thms
    1.10 +(
    1.11 +  val name = @{binding algebra}
    1.12    val description = "pre-simplification rules for algebraic methods"
    1.13  )
    1.14  *}