* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
authorwenzelm
Wed Jun 13 11:54:03 2007 +0200 (2007-06-13)
changeset 23369227c51012cdb
parent 23368 ad690b9bca1c
child 23370 513a8ee192f1
* 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;
NEWS
     1.1 --- a/NEWS	Wed Jun 13 11:16:24 2007 +0200
     1.2 +++ b/NEWS	Wed Jun 13 11:54:03 2007 +0200
     1.3 @@ -154,6 +154,21 @@
     1.4  Command 'print_theory' outputs the normalized system of recursive
     1.5  equations, see section "definitions".
     1.6  
     1.7 +* Isar: method "assumption" (and implicit closing of subproofs) now
     1.8 +takes simple non-atomic goal assumptions into account: after applying
     1.9 +an assumption as a rule the resulting subgoals are solved by atomic
    1.10 +assumption steps.  This is particularly useful to finish 'obtain'
    1.11 +goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis",
    1.12 +without referring to the original premise "!!x. P x ==> thesis" in the
    1.13 +Isar proof context.  POTENTIAL INCOMPATIBILITY: method "assumption" is
    1.14 +more permissive.
    1.15 +
    1.16 +* Isar: implicit use of prems from the Isar proof context is
    1.17 +considered a legacy feature.  Common applications like ``have A .''
    1.18 +may be replaced by ``have A by fact'' or ``note `A`''.  In general,
    1.19 +referencing facts explicitly here improves readability and
    1.20 +maintainability of proof texts.
    1.21 +
    1.22  * Isar: improper proof element 'guess' is like 'obtain', but derives
    1.23  the obtained context from the course of reasoning!  For example:
    1.24