src/HOL/Arith.ML
changeset 6079 4f7975c74cdf
parent 6075 c148037f53c6
child 6101 dde00dc06f0d
     1.1 --- a/src/HOL/Arith.ML	Mon Jan 11 12:52:53 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Mon Jan 11 16:50:49 1999 +0100
     1.3 @@ -855,12 +855,11 @@
     1.4  val not_lessD = leI;
     1.5  val sym = sym;
     1.6  
     1.7 -fun mkEqTrue thm = thm RS (eqTrueI RS eq_reflection);
     1.8 +val mk_Eq = mk_eq;
     1.9  val mk_Trueprop = HOLogic.mk_Trueprop;
    1.10  
    1.11 -fun neg_prop(TP$(Const("Not",_)$t)) = (TP$t, true)
    1.12 -  | neg_prop(TP$t) =
    1.13 -      (TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t), false);
    1.14 +fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
    1.15 +  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
    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))