
diff -r 7808fbc9c3b4 -r 30bcceed0dc2 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Apr 24 21:29:22 2010 -0700
+++ b/src/HOL/Fields.thy	Sun Apr 25 08:25:34 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




