# HG changeset patch
# User haftmann
# Date 1325162501 -3600
# Node ID 6fc579c917b8d91ada6fb71bc8643e363476b7df
# Parent  0da934e135b089b4688e3f0c4017afd631c035f3
qualified Finite_Set.fold

diff -r 0da934e135b0 -r 6fc579c917b8 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Dec 29 10:47:56 2011 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Dec 29 13:41:41 2011 +0100
@@ -1222,13 +1222,13 @@
   "class.ab_semigroup_idem_mult inf"
 proof qed (rule inf_assoc inf_commute inf_idem)+
 
-lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
+lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold inf b (insert a A) = inf a (Finite_Set.fold inf b A)"
 by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
 
-lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
+lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> Finite_Set.fold inf c A"
 by (induct pred: finite) (auto intro: le_infI1)
 
-lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
+lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> Finite_Set.fold inf b A \<le> inf a b"
 proof(induct arbitrary: a pred:finite)
   case empty thus ?case by simp
 next
@@ -1292,13 +1292,13 @@
 lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
 
-lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
+lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold sup b (insert a A) = sup a (Finite_Set.fold sup b A)"
 by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
 
-lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
+lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> Finite_Set.fold sup c A \<le> sup b c"
 by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
 
-lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
+lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> Finite_Set.fold sup b A"
 by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
 
 end
diff -r 0da934e135b0 -r 6fc579c917b8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Dec 29 10:47:56 2011 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Dec 29 13:41:41 2011 +0100
@@ -2269,4 +2269,6 @@
     by simp
 qed
 
+hide_const (open) Finite_Set.fold
+
 end
diff -r 0da934e135b0 -r 6fc579c917b8 src/HOL/More_List.thy
--- a/src/HOL/More_List.thy	Thu Dec 29 10:47:56 2011 +0100
+++ b/src/HOL/More_List.thy	Thu Dec 29 13:41:41 2011 +0100
@@ -6,8 +6,6 @@
 imports List
 begin
 
-hide_const (open) Finite_Set.fold
-
 text {* Fold combinator with canonical argument order *}
 
 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where