--- a/src/HOL/Finite_Set.thy Tue Mar 09 04:22:50 2004 +0100
+++ b/src/HOL/Finite_Set.thy Wed Mar 10 10:34:49 2004 +0100
@@ -30,7 +30,7 @@
lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
plus_ac0.zero plus_ac0_zero_right
-instance semiring < plus_ac0
+instance almost_semiring < plus_ac0
proof qed (rule add_commute add_assoc almost_semiring.add_0)+
axclass times_ac1 < times, one
@@ -59,7 +59,7 @@
finally show ?thesis .
qed
-instance semiring < times_ac1
+instance almost_semiring < times_ac1
apply intro_classes
apply (rule mult_commute)
apply (rule mult_assoc, simp)