src/HOL/Orderings.ML
changeset 15780 6744bba5561d
parent 15524 2ef571f80a55
child 15791 446ec11266be
     1.1 --- a/src/HOL/Orderings.ML	Wed Apr 20 16:03:17 2005 +0200
     1.2 +++ b/src/HOL/Orderings.ML	Wed Apr 20 17:19:18 2005 +0200
     1.3 @@ -39,9 +39,7 @@
     1.4  val le_maxI1 = thm "le_maxI1";
     1.5  val le_maxI2 = thm "le_maxI2";
     1.6  val less_max_iff_disj = thm "less_max_iff_disj";
     1.7 -val max_le_iff_conj = thm "max_le_iff_conj";
     1.8  val max_less_iff_conj = thm "max_less_iff_conj";
     1.9 -val le_min_iff_conj = thm "le_min_iff_conj";
    1.10  val min_less_iff_conj = thm "min_less_iff_conj";
    1.11  val min_le_iff_disj = thm "min_le_iff_disj";
    1.12  val min_less_iff_disj = thm "min_less_iff_disj";