| changeset 68547 | 549a4992222f |
| parent 68529 | 29235951f104 |
| parent 68536 | e14848001c4c |
| child 69593 | 3dda49e08b9d |
--- a/src/HOL/Rat.thy Fri Jun 29 15:22:30 2018 +0100 +++ b/src/HOL/Rat.thy Fri Jun 29 22:14:33 2018 +0200 @@ -529,6 +529,10 @@ end +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 + + instantiation rat :: distrib_lattice begin