src/HOL/Finite_Set.thy

   assumes "finite A"
   shows "inf B (Inf A) = fold inf B A"
 proof -
   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: Inf_insert inf_commute fold_fun_comm)
+    (simp_all add: inf_commute fold_fun_comm)
 qed
 
 lemma sup_Sup_fold_sup:
   assumes "finite A"
   shows "sup B (Sup A) = fold sup B A"
 proof -
   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: Sup_insert sup_commute fold_fun_comm)
+    (simp_all add: sup_commute fold_fun_comm)
 qed
 
 lemma Inf_fold_inf:
   assumes "finite A"
   shows "Inf A = fold inf top A"

 proof (rule sym)
   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
   from `finite A` show "?fold = ?inf"
     by (induct A arbitrary: B)
-      (simp_all add: INFI_def Inf_insert inf_left_commute)
+      (simp_all add: INFI_def inf_left_commute)
 qed
 
 lemma sup_SUPR_fold_sup:
   assumes "finite A"
   shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
 proof (rule sym)
   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
   from `finite A` show "?fold = ?sup"
     by (induct A arbitrary: B)
-      (simp_all add: SUPR_def Sup_insert sup_left_commute)
+      (simp_all add: SUPR_def sup_left_commute)
 qed
 
 lemma INFI_fold_inf:
   assumes "finite A"
   shows "INFI A f = fold (inf \<circ> f) top A"