# HG changeset patch
# User wenzelm
# Date 1010621458 -3600
# Node ID 827818b891c786dcd302cf757cd9a4b72f026d9a
# Parent  df42e9a53a0213b11d7425add1fed6e216d59a9e
qualified exports from locales;

diff -r df42e9a53a02 -r 827818b891c7 src/HOL/Finite_Set.ML
--- a/src/HOL/Finite_Set.ML	Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/Finite_Set.ML	Thu Jan 10 01:10:58 2002 +0100
@@ -97,18 +97,18 @@
 val finite_subset = thm "finite_subset";
 val finite_subset_induct = thm "finite_subset_induct";
 val finite_trancl = thm "finite_trancl";
-val foldSet_determ = thm "foldSet_determ";
+val foldSet_determ = thm "LC.foldSet_determ";
 val foldSet_imp_finite = thm "foldSet_imp_finite";
-val fold_Un_Int = thm "fold_Un_Int";
-val fold_Un_disjoint = thm "fold_Un_disjoint";
-val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
-val fold_commute = thm "fold_commute";
+val fold_Un_Int = thm "ACe.fold_Un_Int";
+val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
+val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
+val fold_commute = thm "LC.fold_commute";
 val fold_def = thm "fold_def";
 val fold_empty = thm "fold_empty";
-val fold_equality = thm "fold_equality";
-val fold_insert = thm "fold_insert";
-val fold_nest_Un_Int = thm "fold_nest_Un_Int";
-val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
+val fold_equality = thm "LC.fold_equality";
+val fold_insert = thm "LC.fold_insert";
+val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
+val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
 val n_sub_lemma = thm "n_sub_lemma";
 val n_subsets = thm "n_subsets";
 val psubset_card_mono = thm "psubset_card_mono";
diff -r df42e9a53a02 -r 827818b891c7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Jan 10 01:10:58 2002 +0100
@@ -711,7 +711,7 @@
     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)
@@ -722,7 +722,7 @@
     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:
@@ -746,13 +746,13 @@
     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
@@ -777,7 +777,7 @@
 
 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")
diff -r df42e9a53a02 -r 827818b891c7 src/HOL/NumberTheory/IntFact.thy
--- a/src/HOL/NumberTheory/IntFact.thy	Wed Jan 09 17:56:46 2002 +0100
+++ b/src/HOL/NumberTheory/IntFact.thy	Thu Jan 10 01:10:58 2002 +0100
@@ -40,7 +40,7 @@
 lemma setprod_insert [simp]:
     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
   apply (unfold setprod_def)
-  apply (simp add: zmult_left_commute fold_insert [standard])
+  apply (simp add: zmult_left_commute LC.fold_insert)
   done