src/HOL/Finite_Set.thy

 
 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" (!??) *)
 
-lemma (in ACe [simp]) left_ident: "e \<cdot> x = x"
+lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"
 proof -
   have "x \<cdot> e = x" by (rule ident)
   thus ?thesis by (subst commute)
 qed
 
 lemma (in ACe) fold_Un_Int:
   "finite A ==> finite B ==>
     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"
   apply (induct set: Finites)
    apply simp
-  apply (simp add: AC fold_insert insert_absorb Int_insert_left)
+  apply (simp add: AC LC.fold_insert insert_absorb Int_insert_left)
   done
 
 lemma (in ACe) fold_Un_disjoint:
   "finite A ==> finite B ==> A Int B = {} ==>
     fold f e (A Un B) = fold f e A \<cdot> fold f e B"

   next
     case (insert F x)
     have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
       by simp
     also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
-      by (rule fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)
+      by (rule LC.fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)
     also from insert have "fold (f \<circ> g) e (F \<union> B) =
       fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
     also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
       by (simp add: AC)
     also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
-      by (rule fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
+      by (rule LC.fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)
     finally show ?case .
   qed
 qed
 
 

 lemma setsum_empty [simp]: "setsum f {} = 0"
   by (simp add: setsum_def)
 
 lemma setsum_insert [simp]:
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
-  by (simp add: setsum_def fold_insert plus_ac0_left_commute)
+  by (simp add: setsum_def LC.fold_insert plus_ac0_left_commute)
 
 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"
   apply (case_tac "finite A")
    prefer 2 apply (simp add: setsum_def)
   apply (erule finite_induct)