src/HOL/Arith.ML
changeset 6109 82b50115564c
parent 6101 dde00dc06f0d
child 6115 c70bce7deb0f
     1.1 --- a/src/HOL/Arith.ML	Tue Jan 12 17:19:53 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Jan 13 08:41:28 1999 +0100
     1.3 @@ -852,6 +852,7 @@
     1.4  val neqE = linorder_neqE;
     1.5  val notI = notI;
     1.6  val sym = sym;
     1.7 +val not_lessD = linorder_not_less RS iffD1;
     1.8  
     1.9  val mk_Eq = mk_eq;
    1.10  val mk_Trueprop = HOLogic.mk_Trueprop;
    1.11 @@ -870,7 +871,6 @@
    1.12  
    1.13  val lessD = Suc_leI;
    1.14  val not_leD = not_leE RS Suc_leI;
    1.15 -val not_lessD = leI;
    1.16  
    1.17  (* Turn term into list of summand * multiplicity plus a constant *)
    1.18  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))