| changeset 51540 | eea5c4ca4a0e |
| parent 51489 | f738e6dbd844 |
| child 51548 | 757fa47af981 |
--- a/src/HOL/List.thy Tue Mar 26 15:10:28 2013 +0100 +++ b/src/HOL/List.thy Tue Mar 26 20:49:57 2013 +0100 @@ -2783,8 +2783,8 @@ declare Inf_fin.set_eq_fold [code] declare Sup_fin.set_eq_fold [code] -declare min_max.Inf_fin.set_eq_fold [code] -declare min_max.Sup_fin.set_eq_fold [code] +declare Min.set_eq_fold [code] +declare Max.set_eq_fold [code] lemma (in complete_lattice) Inf_set_fold: "Inf (set xs) = fold inf xs top"