# HG changeset patch
# User wenzelm
# Date 1235827064 -3600
# Node ID faf95eb3f3759475a167c3be1d312d3d68daca06
# Parent  097673d2e50f4f4efcd6187461494c6d982b164b
* New prover for coherent logic (see src/Tools/coherent.ML).

diff -r 097673d2e50f -r faf95eb3f375 NEWS
--- a/NEWS	Sat Feb 28 14:17:27 2009 +0100
+++ b/NEWS	Sat Feb 28 14:17:44 2009 +0100
@@ -64,6 +64,8 @@
 * There is a new syntactic category "float_const" for signed decimal
 fractions (e.g. 123.45 or -123.45).
 
+* New prover for coherent logic (see src/Tools/coherent.ML).
+
 
 *** Pure ***