src/HOL/Groups.thy
changeset 59557 ebd8ecacfba6
parent 59322 8ccecf1415b0
child 59559 35da1bbf234e
     1.1 --- a/src/HOL/Groups.thy	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/src/HOL/Groups.thy	Thu Feb 19 11:53:36 2015 +0100
     1.3 @@ -518,11 +518,11 @@
     1.4  
     1.5  class ab_group_add = minus + uminus + comm_monoid_add +
     1.6    assumes ab_left_minus: "- a + a = 0"
     1.7 -  assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
     1.8 +  assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
     1.9  begin
    1.10  
    1.11  subclass group_add
    1.12 -  proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
    1.13 +  proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
    1.14  
    1.15  subclass cancel_comm_monoid_add
    1.16  proof
    1.17 @@ -1375,6 +1375,7 @@
    1.18  
    1.19  end
    1.20  
    1.21 +hide_fact (open) ab_diff_conv_add_uminus add_imp_eq
    1.22  
    1.23  subsection {* Tools setup *}
    1.24