src/HOL/Library/Set_Algebras.thy
changeset 60679 ade12ef2773c
parent 60500 903bb1495239
child 61337 4645502c3c64
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -64,28 +64,28 @@
     1.4    "x =o A \<equiv> x \<in> A"
     1.5  
     1.6  instance set :: (semigroup_add) semigroup_add
     1.7 -  by default (force simp add: set_plus_def add.assoc)
     1.8 +  by standard (force simp add: set_plus_def add.assoc)
     1.9  
    1.10  instance set :: (ab_semigroup_add) ab_semigroup_add
    1.11 -  by default (force simp add: set_plus_def add.commute)
    1.12 +  by standard (force simp add: set_plus_def add.commute)
    1.13  
    1.14  instance set :: (monoid_add) monoid_add
    1.15 -  by default (simp_all add: set_plus_def)
    1.16 +  by standard (simp_all add: set_plus_def)
    1.17  
    1.18  instance set :: (comm_monoid_add) comm_monoid_add
    1.19 -  by default (simp_all add: set_plus_def)
    1.20 +  by standard (simp_all add: set_plus_def)
    1.21  
    1.22  instance set :: (semigroup_mult) semigroup_mult
    1.23 -  by default (force simp add: set_times_def mult.assoc)
    1.24 +  by standard (force simp add: set_times_def mult.assoc)
    1.25  
    1.26  instance set :: (ab_semigroup_mult) ab_semigroup_mult
    1.27 -  by default (force simp add: set_times_def mult.commute)
    1.28 +  by standard (force simp add: set_times_def mult.commute)
    1.29  
    1.30  instance set :: (monoid_mult) monoid_mult
    1.31 -  by default (simp_all add: set_times_def)
    1.32 +  by standard (simp_all add: set_times_def)
    1.33  
    1.34  instance set :: (comm_monoid_mult) comm_monoid_mult
    1.35 -  by default (simp_all add: set_times_def)
    1.36 +  by standard (simp_all add: set_times_def)
    1.37  
    1.38  lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
    1.39    by (auto simp add: set_plus_def)