src/HOL/Lattices.thy
changeset 22139 539a63b98f76
parent 22068 00bed5ac9884
child 22168 627e7aee1b82
     1.1 --- a/src/HOL/Lattices.thy	Sat Jan 20 14:09:23 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sat Jan 20 14:09:27 2007 +0100
     1.3 @@ -280,26 +280,26 @@
     1.4  text {* ML legacy bindings *}
     1.5  
     1.6  ML {*
     1.7 -val Least_def = thm "Least_def";
     1.8 -val Least_equality = thm "Least_equality";
     1.9 -val min_def = thm "min_def";
    1.10 -val min_of_mono = thm "min_of_mono";
    1.11 -val max_def = thm "max_def";
    1.12 -val max_of_mono = thm "max_of_mono";
    1.13 -val min_leastL = thm "min_leastL";
    1.14 -val max_leastL = thm "max_leastL";
    1.15 -val min_leastR = thm "min_leastR";
    1.16 -val max_leastR = thm "max_leastR";
    1.17 -val le_max_iff_disj = thm "le_max_iff_disj";
    1.18 -val le_maxI1 = thm "le_maxI1";
    1.19 -val le_maxI2 = thm "le_maxI2";
    1.20 -val less_max_iff_disj = thm "less_max_iff_disj";
    1.21 -val max_less_iff_conj = thm "max_less_iff_conj";
    1.22 -val min_less_iff_conj = thm "min_less_iff_conj";
    1.23 -val min_le_iff_disj = thm "min_le_iff_disj";
    1.24 -val min_less_iff_disj = thm "min_less_iff_disj";
    1.25 -val split_min = thm "split_min";
    1.26 -val split_max = thm "split_max";
    1.27 +val Least_def = @{thm Least_def}
    1.28 +val Least_equality = @{thm Least_equality}
    1.29 +val min_def = @{thm min_def}
    1.30 +val min_of_mono = @{thm min_of_mono}
    1.31 +val max_def = @{thm max_def}
    1.32 +val max_of_mono = @{thm max_of_mono}
    1.33 +val min_leastL = @{thm min_leastL}
    1.34 +val max_leastL = @{thm max_leastL}
    1.35 +val min_leastR = @{thm min_leastR}
    1.36 +val max_leastR = @{thm max_leastR}
    1.37 +val le_max_iff_disj = @{thm le_max_iff_disj}
    1.38 +val le_maxI1 = @{thm le_maxI1}
    1.39 +val le_maxI2 = @{thm le_maxI2}
    1.40 +val less_max_iff_disj = @{thm less_max_iff_disj}
    1.41 +val max_less_iff_conj = @{thm max_less_iff_conj}
    1.42 +val min_less_iff_conj = @{thm min_less_iff_conj}
    1.43 +val min_le_iff_disj = @{thm min_le_iff_disj}
    1.44 +val min_less_iff_disj = @{thm min_less_iff_disj}
    1.45 +val split_min = @{thm split_min}
    1.46 +val split_max = @{thm split_max}
    1.47  *}
    1.48  
    1.49  end