# HG changeset patch
# User wenzelm
# Date 1582925023 -3600
# Node ID 4c3eedc8e0f7ed8e36671817f628ea65dca8217d
# Parent  a296d3697e50c806e02d2f5fa3470952595feb39
NEWS;

diff -r a296d3697e50 -r 4c3eedc8e0f7 NEWS
--- a/NEWS	Fri Feb 28 21:34:04 2020 +0100
+++ b/NEWS	Fri Feb 28 22:23:43 2020 +0100
@@ -136,6 +136,10 @@
 * More scalable Export.export using XML.tree to avoid premature string
 allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
 
+* Prover IDE support for the underlying Poly/ML compiler (not the basis
+library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
+implementation with full markup.
+
 
 *** System ***