| author | huffman | 
| Tue, 04 Mar 2014 16:16:05 -0800 | |
| changeset 55912 | e12a0ab9917c | 
| parent 55911 | d00023bd3554 | 
| child 55913 | c1409c103b77 | 
| src/HOL/Rings.thy | file | annotate | diff | comparison | revisions | 
--- a/src/HOL/Rings.thy Tue Mar 04 15:26:12 2014 -0800 +++ b/src/HOL/Rings.thy Tue Mar 04 16:16:05 2014 -0800 @@ -1066,7 +1066,7 @@ "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k" by(subst abs_dvd_iff[symmetric]) simp -text {* The following lemmas can be proven in more generale structures, but +text {* The following lemmas can be proven in more general structures, but are dangerous as simp rules in absence of @{thm neg_equal_zero}, @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}