src/HOL/Library/Set_Algebras.thy

--- a/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -64,28 +64,28 @@
   "x =o A \<equiv> x \<in> A"
 
 instance set :: (semigroup_add) semigroup_add
-  by default (force simp add: set_plus_def add.assoc)
+  by standard (force simp add: set_plus_def add.assoc)
 
 instance set :: (ab_semigroup_add) ab_semigroup_add
-  by default (force simp add: set_plus_def add.commute)
+  by standard (force simp add: set_plus_def add.commute)
 
 instance set :: (monoid_add) monoid_add
-  by default (simp_all add: set_plus_def)
+  by standard (simp_all add: set_plus_def)
 
 instance set :: (comm_monoid_add) comm_monoid_add
-  by default (simp_all add: set_plus_def)
+  by standard (simp_all add: set_plus_def)
 
 instance set :: (semigroup_mult) semigroup_mult
-  by default (force simp add: set_times_def mult.assoc)
+  by standard (force simp add: set_times_def mult.assoc)
 
 instance set :: (ab_semigroup_mult) ab_semigroup_mult
-  by default (force simp add: set_times_def mult.commute)
+  by standard (force simp add: set_times_def mult.commute)
 
 instance set :: (monoid_mult) monoid_mult
-  by default (simp_all add: set_times_def)
+  by standard (simp_all add: set_times_def)
 
 instance set :: (comm_monoid_mult) comm_monoid_mult
-  by default (simp_all add: set_times_def)
+  by standard (simp_all add: set_times_def)
 
 lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
   by (auto simp add: set_plus_def)