src/HOL/Lattices.thy
changeset 21619 dea0914773f7
parent 21381 79e065f2be95
child 21733 131dd2a27137
     1.1 --- a/src/HOL/Lattices.thy	Fri Dec 01 16:08:45 2006 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Fri Dec 01 17:22:28 2006 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Tobias Nipkow
     1.5  *)
     1.6  
     1.7 -header {* Lattices via Locales *}
     1.8 +header {* Abstract lattices *}
     1.9  
    1.10  theory Lattices
    1.11  imports Orderings
    1.12 @@ -187,29 +187,4 @@
    1.13  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
    1.14                 mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
    1.15  
    1.16 -text {* ML legacy bindings *}
    1.17 -
    1.18 -ML {*
    1.19 -val Least_def = thm "Least_def";
    1.20 -val Least_equality = thm "Least_equality";
    1.21 -val min_def = thm "min_def";
    1.22 -val min_of_mono = thm "min_of_mono";
    1.23 -val max_def = thm "max_def";
    1.24 -val max_of_mono = thm "max_of_mono";
    1.25 -val min_leastL = thm "min_leastL";
    1.26 -val max_leastL = thm "max_leastL";
    1.27 -val min_leastR = thm "min_leastR";
    1.28 -val max_leastR = thm "max_leastR";
    1.29 -val le_max_iff_disj = thm "le_max_iff_disj";
    1.30 -val le_maxI1 = thm "le_maxI1";
    1.31 -val le_maxI2 = thm "le_maxI2";
    1.32 -val less_max_iff_disj = thm "less_max_iff_disj";
    1.33 -val max_less_iff_conj = thm "max_less_iff_conj";
    1.34 -val min_less_iff_conj = thm "min_less_iff_conj";
    1.35 -val min_le_iff_disj = thm "min_le_iff_disj";
    1.36 -val min_less_iff_disj = thm "min_less_iff_disj";
    1.37 -val split_min = thm "split_min";
    1.38 -val split_max = thm "split_max";
    1.39 -*}
    1.40 -
    1.41  end