src/HOL/Rat.thy
changeset 70344 050104f01bf9
parent 69593 3dda49e08b9d
child 70345 80a1aa30e24d
equal deleted inserted replaced
70343:e54caaa38ad9 70344:050104f01bf9
   527     done
   527     done
   528 qed
   528 qed
   529 
   529 
   530 end
   530 end
   531 
   531 
       
   532 text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
       
   533 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
       
   534 explosions.\<close>
       
   535 
   532 lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   536 lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   533 lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   537 lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   534 
   538 
   535 
   539 
   536 instantiation rat :: distrib_lattice
   540 instantiation rat :: distrib_lattice