src/HOL/Finite_Set.thy
changeset 14449 d5c3d21df790
parent 14443 75910c7557c5
child 14485 ea2707645af8
--- 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)