avoid pseudo-collection to be used in generated proofs
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago ago)
changeset 7053080a1aa30e24d
parent 70529 050104f01bf9
child 70531 408e15cbd2a6
avoid pseudo-collection to be used in generated proofs
src/HOL/Rat.thy
     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 @@ -533,8 +533,8 @@
     1.4  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.5  explosions.\<close>
     1.6  
     1.7 -lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
     1.8 -lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
     1.9 +lemmas (in linordered_field) sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
    1.10 +lemmas sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
    1.11  
    1.12  
    1.13  instantiation rat :: distrib_lattice