--- a/NEWS Wed Jan 13 16:01:03 2016 +0100
+++ b/NEWS Wed Jan 13 16:41:32 2016 +0100
@@ -9,6 +9,12 @@
*** General ***
+* Eisbach is now based on Pure instead of HOL. Objects-logics may import
+either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or
+~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that
+the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further
+examples that do require HOL.
+
* Better resource usage on all platforms (Linux, Windows, Mac OS X) for
both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage.