# HG changeset patch
# User wenzelm
# Date 1446634402 -3600
# Node ID e7d4dac7a79fff8631f32d67ef2c86165c1bd4ef
# Parent  c3d6e570ccefff8d6add2f945ad7fdf81e0bd432
NEWS;

diff -r c3d6e570ccef -r e7d4dac7a79f NEWS
--- a/NEWS	Wed Nov 04 08:13:52 2015 +0100
+++ b/NEWS	Wed Nov 04 11:53:22 2015 +0100
@@ -575,6 +575,9 @@
 * Bash shell function "jvmpath" has been renamed to "platform_path": it
 is relevant both for Poly/ML and JVM processes.
 
+* Heap images are 10-15% smaller due to less wasteful persistent theory
+content (using ML type theory_id instead of theory);
+
 
 
 New in Isabelle2015 (May 2015)