--- a/NEWS Wed Oct 02 22:01:04 2019 +0200
+++ b/NEWS Fri Oct 04 15:30:52 2019 +0200
@@ -58,6 +58,12 @@
*** HOL ***
+* Term_XML.Encode/Decode.term uses compact representation of Const
+"typargs" from the given declaration environment. This also makes more
+sense for translations to lambda-calculi with explicit polymorphism.
+INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
+applications.
+
* ASCII membership syntax concerning big operators for infimum and
supremum is gone. INCOMPATIBILITY.
@@ -99,6 +105,7 @@
libraries. See also the module Export_Theory in Isabelle/Scala.
+
New in Isabelle2019 (June 2019)
-------------------------------