src/HOL/OrderedGroup.thy
changeset 31902 862ae16a799d
parent 31034 736f521ad036
child 32010 cb1a1c94b4cd
child 32064 53ca12ff305d
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -22,13 +22,15 @@
     1.4    \end{itemize}
     1.5  *}
     1.6  
     1.7 -ML{*
     1.8 -structure AlgebraSimps =
     1.9 -  NamedThmsFun(val name = "algebra_simps"
    1.10 -               val description = "algebra simplification rules");
    1.11 +ML {*
    1.12 +structure Algebra_Simps = Named_Thms
    1.13 +(
    1.14 +  val name = "algebra_simps"
    1.15 +  val description = "algebra simplification rules"
    1.16 +)
    1.17  *}
    1.18  
    1.19 -setup AlgebraSimps.setup
    1.20 +setup Algebra_Simps.setup
    1.21  
    1.22  text{* The rewrites accumulated in @{text algebra_simps} deal with the
    1.23  classical algebraic structures of groups, rings and family. They simplify