*** empty log message ***
authornipkow
Tue Aug 13 21:59:44 2002 +0200 (2002-08-13)
changeset 135002222c7a0e8bb
parent 13499 f95f5818f24f
child 13501 79242cccaddc
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Tue Aug 13 21:57:15 2002 +0200
     1.2 +++ b/NEWS	Tue Aug 13 21:59:44 2002 +0200
     1.3 @@ -40,6 +40,9 @@
     1.4  * attribute [symmetric] now works for relations as well; it turns
     1.5  (x,y) : R^-1 into (y,x) : R, and vice versa;
     1.6  
     1.7 +* arith(_tac) now produces a counter example if it cannot prove a theorem.
     1.8 +  In ProofGeneral the counter example appears in the trace buffer.
     1.9 +
    1.10  * arith(_tac) does now know about div k and mod k where k is a numeral
    1.11  of type nat or int. It can solve simple goals like
    1.12