# HG changeset patch
# User haftmann
# Date 1560501267 0
# Node ID 050104f01bf9c70d25167f32e8f70f8e730c2a2c
# Parent  e54caaa38ad991b50d38c7b7e0fcef5ae6330547
moved comment to approproiate place

diff -r e54caaa38ad9 -r 050104f01bf9 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Fields.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -900,10 +900,6 @@
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
   by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
 
-text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
-of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
-explosions.\<close>
-
 lemma divide_pos_pos[simp]:
   "0 < x ==> 0 < y ==> 0 < x / y"
 by(simp add:field_simps)
diff -r e54caaa38ad9 -r 050104f01bf9 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -529,6 +529,10 @@
 
 end
 
+text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
+of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
+explosions.\<close>
+
 lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
 lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff