src/HOL/Groups.thy

 imports Orderings
 uses ("~~/src/Provers/Arith/abel_cancel.ML")
 begin
 
 subsection {* Fact collections *}
+
+ML {*
+structure Ac_Simps = Named_Thms(
+  val name = "ac_simps"
+  val description = "associativity and commutativity simplification rules"
+)
+*}
+
+setup Ac_Simps.setup
 
 ML {*
 structure Algebra_Simps = Named_Thms(
   val name = "algebra_simps"
   val description = "algebra simplification rules"

 products into a canonical form (by ordered rewriting). As a result it decides
 group and ring equalities but also helps with inequalities.
 
 Of course it also works for fields, but it knows nothing about multiplicative
 inverses or division. This is catered for by @{text field_simps}. *}
-
-
-ML {*
-structure Ac_Simps = Named_Thms(
-  val name = "ac_simps"
-  val description = "associativity and commutativity simplification rules"
-)
-*}
-
-setup Ac_Simps.setup
 
 
 subsection {* Abstract structures *}
 
 text {*