src/HOL/Library/Set_Algebras.thy

   apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
    apply (rule_tac x = "aa + ba" in exI)
    apply (auto simp add: ac_simps)
   done
 
-theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
+lemmas set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   set_plus_rearrange3 set_plus_rearrange4
 
 lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
   by (auto simp add: elt_set_plus_def)
 

   apply (auto simp add: elt_set_times_def set_times_def ac_simps)
    apply (rule_tac x = "aa * ba" in exI)
    apply (auto simp add: ac_simps)
   done
 
-theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
+lemmas set_times_rearranges = set_times_rearrange set_times_rearrange2
   set_times_rearrange3 set_times_rearrange4
 
 lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
   by (auto simp add: elt_set_times_def)
 

     elt_set_plus_def elt_set_times_def set_times_def
     set_plus_def ring_distribs)
   apply auto
   done
 
-theorems set_times_plus_distribs =
+lemmas set_times_plus_distribs =
   set_times_plus_distrib
   set_times_plus_distrib2
 
 lemma set_neg_intro: "(a::'a::ring_1) \<in> (- 1) *o C \<Longrightarrow> - a \<in> C"
   by (auto simp add: elt_set_times_def)