--- a/src/HOL/Library/SetsAndFunctions.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Thu Mar 26 20:08:55 2009 +0100
@@ -107,26 +107,26 @@
apply simp
done
-interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
+interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_assoc)
done
-interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
+interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_assoc)
done
-interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
+interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
apply default
apply (unfold set_plus_def)
apply (force simp add: add_ac)
apply force
done
-interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
+interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
apply default
apply (unfold set_times_def)
apply (force simp add: mult_ac)