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.9     apply (rule_tac x = "aa + ba" in exI)
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.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
```