src/HOL/Library/Set_Algebras.thy
changeset 44142 8e27e0177518
parent 40887 ee8d0548c148
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -153,7 +153,7 @@
     1.4  
     1.5  theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
     1.6      a +o (C \<oplus> D)"
     1.7 -  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
     1.8 +  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
     1.9     apply (rule_tac x = "aa + ba" in exI)
    1.10     apply (auto simp add: add_ac)
    1.11    done
    1.12 @@ -211,7 +211,7 @@
    1.13    by (auto simp add: elt_set_plus_def)
    1.14  
    1.15  lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
    1.16 -  apply (auto intro!: subsetI simp add: set_plus_def)
    1.17 +  apply (auto simp add: set_plus_def)
    1.18    apply (rule_tac x = 0 in bexI)
    1.19     apply (rule_tac x = x in bexI)
    1.20      apply (auto simp add: add_ac)
    1.21 @@ -264,7 +264,7 @@
    1.22  
    1.23  theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
    1.24      a *o (C \<otimes> D)"
    1.25 -  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
    1.26 +  apply (auto simp add: elt_set_times_def set_times_def
    1.27      mult_ac)
    1.28     apply (rule_tac x = "aa * ba" in exI)
    1.29     apply (auto simp add: mult_ac)
    1.30 @@ -336,7 +336,7 @@
    1.31  
    1.32  lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
    1.33      a *o D \<oplus> C \<otimes> D"
    1.34 -  apply (auto intro!: subsetI simp add:
    1.35 +  apply (auto simp add:
    1.36      elt_set_plus_def elt_set_times_def set_times_def
    1.37      set_plus_def ring_distribs)
    1.38    apply auto