src/HOL/Groups.thy
changeset 63145 703edebd1d92
parent 62608 19f87fa0cfcb
child 63290 9ac558ab0906
     1.1 --- a/src/HOL/Groups.thy	Tue May 24 22:46:23 2016 +0200
     1.2 +++ b/src/HOL/Groups.thy	Wed May 25 11:49:40 2016 +0200
     1.3 @@ -1378,7 +1378,7 @@
     1.4    using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
     1.5  
     1.6  lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
     1.7 -  -- \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
     1.8 +  \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
     1.9  
    1.10  end
    1.11