--- a/src/HOL/Fields.thy Fri Apr 11 17:53:16 2014 +0200 +++ b/src/HOL/Fields.thy Fri Apr 11 22:53:33 2014 +0200 @@ -801,7 +801,7 @@ done *) -lemma divide_pos_pos: +lemma divide_pos_pos[simp]: "0 < x ==> 0 < y ==> 0 < x / y" by(simp add:field_simps)