# HG changeset patch # User webertj # Date 1143032789 -3600 # Node ID 958d5c8a8306fa0672e4de698574c8db1a07fa72 # Parent 3d383e78b6f4872e60a6f9c199d9ed5844cbb525 comment fixed diff -r 3d383e78b6f4 -r 958d5c8a8306 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Wed Mar 22 12:33:44 2006 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Mar 22 14:06:29 2006 +0100 @@ -42,8 +42,8 @@ mk_Eq(in) = `in == True' where `in' is an (in)equality. -neg_prop(t) = neg if t is wrapped up in Trueprop and - nt is the (logically) negated version of t, where the negation +neg_prop(t) = neg if t is wrapped up in Trueprop and + neg is the (logically) negated version of t, where the negation of a negative term is the term itself (no double negation!); is_nat(parameter-types,t) = t:nat