--- a/src/HOL/Groups.thy Sat Apr 24 21:29:22 2010 -0700
+++ b/src/HOL/Groups.thy Sun Apr 25 08:25:34 2010 +0200
@@ -12,6 +12,15 @@
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"
@@ -30,16 +39,6 @@
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 {*