# HG changeset patch
# User wenzelm
# Date 1181728443 -7200
# Node ID 227c51012cdb8bc2981057502416a4e953e0fd0c
# Parent  ad690b9bca1c232920a4ffa5a20fd36870b5401e
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
* Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

diff -r ad690b9bca1c -r 227c51012cdb NEWS
--- a/NEWS	Wed Jun 13 11:16:24 2007 +0200
+++ b/NEWS	Wed Jun 13 11:54:03 2007 +0200
@@ -154,6 +154,21 @@
 Command 'print_theory' outputs the normalized system of recursive
 equations, see section "definitions".
 
+* Isar: method "assumption" (and implicit closing of subproofs) now
+takes simple non-atomic goal assumptions into account: after applying
+an assumption as a rule the resulting subgoals are solved by atomic
+assumption steps.  This is particularly useful to finish 'obtain'
+goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis",
+without referring to the original premise "!!x. P x ==> thesis" in the
+Isar proof context.  POTENTIAL INCOMPATIBILITY: method "assumption" is
+more permissive.
+
+* Isar: implicit use of prems from the Isar proof context is
+considered a legacy feature.  Common applications like ``have A .''
+may be replaced by ``have A by fact'' or ``note `A`''.  In general,
+referencing facts explicitly here improves readability and
+maintainability of proof texts.
+
 * Isar: improper proof element 'guess' is like 'obtain', but derives
 the obtained context from the course of reasoning!  For example: