# HG changeset patch
# User wenzelm
# Date 1581880048 -3600
# Node ID 404624eb3a22936f25e3e2d59bfe7d989b3316f4
# Parent  439410bf451928740a5a9f39a9a7222319b86b33
NEWS;

diff -r 439410bf4519 -r 404624eb3a22 NEWS
--- a/NEWS	Sun Feb 16 17:24:10 2020 +0100
+++ b/NEWS	Sun Feb 16 20:07:28 2020 +0100
@@ -36,6 +36,9 @@
 * Refined treatment of proof terms, including type-class proofs for
 minor object-logics (FOL, FOLP, Sequents).
 
+* The inference kernel is now confined to one main module: structure
+Thm, without the former circular dependency on structure Axclass.
+
 
 *** Isar ***