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