# HG changeset patch
# User wenzelm
# Date 1566331297 -7200
# Node ID 8539476439711230024de2a7238d74dbd6d5e8a8
# Parent  a56b4e59bfd146640f3a1faf2d21276a5d48b305
NEWS;

diff -r a56b4e59bfd1 -r 853947643971 NEWS
--- a/NEWS	Tue Aug 20 20:23:21 2019 +0200
+++ b/NEWS	Tue Aug 20 22:01:37 2019 +0200
@@ -60,6 +60,16 @@
 * Antiquotation @{oracle_name} inlines a formally checked oracle name.
 
 
+*** System ***
+
+* Theory export via Isabelle/Scala has been reworked. The former "fact"
+name space is now split into individual "thm" items: names are
+potentially indexed, such as "foo" for singleton facts, or "bar(1)",
+"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
+exported as well: this spans an overall dependency graph of internal
+inferences; it might help to reconstruct the formal structure of theory
+libraries. See also the module Export_Theory in Isabelle/Scala.
+
 
 New in Isabelle2019 (June 2019)
 -------------------------------