src/HOL/Lattices.thy
changeset 22548 6ce4bddf3bcb
parent 22454 c3654ba76a09
child 22737 d87ccbcc2702
     1.1 --- a/src/HOL/Lattices.thy	Thu Mar 29 11:59:54 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Thu Mar 29 14:21:45 2007 +0200
     1.3 @@ -327,30 +327,4 @@
     1.4  lemmas inf_aci = inf_ACI
     1.5  lemmas sup_aci = sup_ACI
     1.6  
     1.7 -
     1.8 -text {* ML legacy bindings *}
     1.9 -
    1.10 -ML {*
    1.11 -val Least_def = @{thm Least_def}
    1.12 -val Least_equality = @{thm Least_equality}
    1.13 -val min_def = @{thm min_def}
    1.14 -val min_of_mono = @{thm min_of_mono}
    1.15 -val max_def = @{thm max_def}
    1.16 -val max_of_mono = @{thm max_of_mono}
    1.17 -val min_leastL = @{thm min_leastL}
    1.18 -val max_leastL = @{thm max_leastL}
    1.19 -val min_leastR = @{thm min_leastR}
    1.20 -val max_leastR = @{thm max_leastR}
    1.21 -val le_max_iff_disj = @{thm le_max_iff_disj}
    1.22 -val le_maxI1 = @{thm le_maxI1}
    1.23 -val le_maxI2 = @{thm le_maxI2}
    1.24 -val less_max_iff_disj = @{thm less_max_iff_disj}
    1.25 -val max_less_iff_conj = @{thm max_less_iff_conj}
    1.26 -val min_less_iff_conj = @{thm min_less_iff_conj}
    1.27 -val min_le_iff_disj = @{thm min_le_iff_disj}
    1.28 -val min_less_iff_disj = @{thm min_less_iff_disj}
    1.29 -val split_min = @{thm split_min}
    1.30 -val split_max = @{thm split_max}
    1.31 -*}
    1.32 -
    1.33  end