# 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 \prop\ 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.