src/HOL/Groups.thy

 
 end
 
 class ab_group_add = minus + uminus + comm_monoid_add +
   assumes ab_left_minus: "- a + a = 0"
-  assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
+  assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
 begin
 
 subclass group_add
-  proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
+  proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
 
 subclass cancel_comm_monoid_add
 proof
   fix a b c :: 'a
   assume "a + b = a + c"

   finally show "?L \<le> ?R" .
 qed
 
 end
 
+hide_fact (open) ab_diff_conv_add_uminus add_imp_eq
 
 subsection {* Tools setup *}
 
 lemma add_mono_thms_linordered_semiring:
   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"