src/HOL/Rat.thy
changeset 70347 e5cd5471c18a
parent 70345 80a1aa30e24d
child 70350 571ae57313a4
     1.1 --- a/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -529,14 +529,6 @@
     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 [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
    1.12 -lemmas sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
    1.13 -
    1.14 -
    1.15  instantiation rat :: distrib_lattice
    1.16  begin
    1.17