src/HOL/List.thy
changeset 46034 773c0c4994df
parent 46030 51b2f3412a03
child 46125 00cd193a48dc
     1.1 --- a/src/HOL/List.thy	Thu Dec 29 13:41:41 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Dec 29 13:42:21 2011 +0100
     1.3 @@ -2511,11 +2511,11 @@
     1.4  text {* @{const Finite_Set.fold} and @{const foldl} *}
     1.5  
     1.6  lemma (in comp_fun_commute) fold_set_remdups:
     1.7 -  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
     1.8 +  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
     1.9    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
    1.10  
    1.11  lemma (in comp_fun_idem) fold_set:
    1.12 -  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
    1.13 +  "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
    1.14    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
    1.15  
    1.16  lemma (in ab_semigroup_idem_mult) fold1_set:
    1.17 @@ -2530,7 +2530,7 @@
    1.18      case True with xs show ?thesis by simp
    1.19    next
    1.20      case False
    1.21 -    then have "fold1 times (insert y (set ys)) = fold times y (set ys)"
    1.22 +    then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
    1.23        by (simp only: finite_set fold1_eq_fold_idem)
    1.24      with xs show ?thesis by (simp add: fold_set mult_commute)
    1.25    qed