src/HOL/Library/Set_Algebras.thy
changeset 54230 b1d955791529
parent 53596 d29d63460d84
child 56899 9b9f4abaaa7e
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -190,12 +190,12 @@
     1.4    done
     1.5  
     1.6  lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
     1.7 -  by (auto simp add: elt_set_plus_def add_ac diff_minus)
     1.8 +  by (auto simp add: elt_set_plus_def add_ac)
     1.9  
    1.10  lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
    1.11 -  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
    1.12 +  apply (auto simp add: elt_set_plus_def add_ac)
    1.13    apply (subgoal_tac "a = (a + - b) + b")
    1.14 -   apply (rule bexI, assumption, assumption)
    1.15 +   apply (rule bexI, assumption)
    1.16    apply (auto simp add: add_ac)
    1.17    done
    1.18