src/HOL/Rat.thy
changeset 70344 050104f01bf9
parent 69593 3dda49e08b9d
child 70345 80a1aa30e24d
     1.1 --- a/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -529,6 +529,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 +text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
     1.8 +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
     1.9 +explosions.\<close>
    1.10 +
    1.11  lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    1.12  lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    1.13