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 ***