src/HOL/Finite_Set.thy
changeset 56166 9a241bc276cd
parent 56154 f0a927235162
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/Finite_Set.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -1041,7 +1041,7 @@
     1.4    interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
     1.5    from `finite A` show "?fold = ?inf"
     1.6      by (induct A arbitrary: B)
     1.7 -      (simp_all add: INF_def inf_left_commute)
     1.8 +      (simp_all add: inf_left_commute)
     1.9  qed
    1.10  
    1.11  lemma sup_SUP_fold_sup:
    1.12 @@ -1052,7 +1052,7 @@
    1.13    interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    1.14    from `finite A` show "?fold = ?sup"
    1.15      by (induct A arbitrary: B)
    1.16 -      (simp_all add: SUP_def sup_left_commute)
    1.17 +      (simp_all add: sup_left_commute)
    1.18  qed
    1.19  
    1.20  lemma INF_fold_inf: