NEWS
changeset 30163 faf95eb3f375
parent 30106 351fc2f8493d
child 30176 78610979b3c6
     1.1 --- a/NEWS	Sat Feb 28 14:17:27 2009 +0100
     1.2 +++ b/NEWS	Sat Feb 28 14:17:44 2009 +0100
     1.3 @@ -64,6 +64,8 @@
     1.4  * There is a new syntactic category "float_const" for signed decimal
     1.5  fractions (e.g. 123.45 or -123.45).
     1.6  
     1.7 +* New prover for coherent logic (see src/Tools/coherent.ML).
     1.8 +
     1.9  
    1.10  *** Pure ***
    1.11