merged

--- a/src/HOL/Fields.thy	Sun Apr 25 23:26:40 2010 +0200
+++ b/src/HOL/Fields.thy	Mon Apr 26 07:47:18 2010 +0200
@@ -13,6 +13,20 @@
 imports Rings
 begin
 
+text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
+if they can be proved to be non-zero (for equations) or positive/negative
+(for inequations). Can be too aggressive and is therefore separate from the
+more benign @{text algebra_simps}. *}
+
+ML {*
+structure Field_Simps = Named_Thms(
+  val name = "field_simps"
+  val description = "algebra simplification rules for fields"
+)
+*}
+
+setup Field_Simps.setup
+
 class field = comm_ring_1 + inverse +
   assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
   assumes field_divide_inverse: "a / b = a * inverse b"
@@ -112,7 +126,7 @@
   "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
   by (simp add: diff_divide_distrib)
 
-lemmas field_eq_simps[no_atp] = algebra_simps
+lemmas field_eq_simps [field_simps, no_atp] = algebra_simps
   (* pull / out*)
   add_divide_eq_iff divide_add_eq_iff
   diff_divide_eq_iff divide_diff_eq_iff
@@ -475,12 +489,7 @@
   finally show ?thesis .
 qed
 
-text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
-if they can be proved to be non-zero (for equations) or positive/negative
-(for inequations). Can be too aggressive and is therefore separate from the
-more benign @{text algebra_simps}. *}
-
-lemmas field_simps[no_atp] = field_eq_simps
+lemmas [field_simps, no_atp] =
   (* multiply ineqn *)
   pos_divide_less_eq neg_divide_less_eq
   pos_less_divide_eq neg_less_divide_eq

--- a/src/HOL/Groups.thy	Sun Apr 25 23:26:40 2010 +0200
+++ b/src/HOL/Groups.thy	Mon Apr 26 07:47:18 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 {*