src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Wed Jun 27 20:31:22 2018 +0200
+++ b/src/HOL/Rat.thy	Thu Jun 28 21:05:56 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