src/HOL/Finite_Set.thy
changeset 12718 ade42a6c22ad
parent 12693 827818b891c7
child 12937 0c4fd7529467
--- a/src/HOL/Finite_Set.thy	Fri Jan 11 14:44:24 2002 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Jan 11 14:44:58 2002 +0100
@@ -707,9 +707,7 @@
   finally show ?thesis .
 qed
 
-lemma (in ACe)
-    AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"  "x \<cdot> y = y \<cdot> x"  "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-  by (rule assoc, rule commute, rule left_commute)  (* FIXME localize "lemmas" (!??) *)
+lemmas (in ACe) AC = assoc commute left_commute
 
 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
 proof -