# HG changeset patch
# User wenzelm
# Date 1467658135 -7200
# Node ID 8bbd325e89e6f553b26e31b9c8dd6751c4974440
# Parent  4270da3064428d19acb0847fea9d0182cf9412a8
NEWS;

diff -r 4270da306442 -r 8bbd325e89e6 NEWS
--- 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.