# HG changeset patch
# User wenzelm
# Date 1010756698 -3600
# Node ID ade42a6c22ad85ea46bdc80bf1d1e3ed597fa1a1
# Parent  2d6b5e22e05dc35defeb442c3d67e4cce2d84b87
lemmas (in ACe) AC;

diff -r 2d6b5e22e05d -r ade42a6c22ad src/HOL/Finite_Set.thy
--- 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 -