--- 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