--- a/NEWS Mon Jul 04 20:33:47 2016 +0200
+++ b/NEWS Mon Jul 04 20:48:55 2016 +0200
@@ -49,6 +49,9 @@
context. Unlike "context includes ... begin", the effect of 'unbundle'
on the target context persists, until different declarations are given.
+* Proof method "blast" is more robust wrt. corner cases of Pure
+statements without object-logic judgment.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
@@ -84,6 +87,13 @@
*** Isar ***
+* The defining position of a literal fact \<open>prop\<close> is maintained more
+carefully, and made accessible as hyperlink in the Prover IDE.
+
+* Commands 'finally' and 'ultimately' used to expose the result as
+literal fact: this accidental behaviour has been discontinued. Rare
+INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
+
* Command 'axiomatization' has become more restrictive to correspond
better to internal axioms as singleton facts with mandatory name. Minor
INCOMPATIBILITY.