NEWS
changeset 56232 31e283f606e2
parent 56218 1c3f1f2431f9
child 56245 84fc7dfa3cd4
     1.1 --- a/NEWS	Thu Mar 20 21:07:57 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 20 22:00:13 2014 +0100
     1.3 @@ -25,6 +25,15 @@
     1.4  supports input methods via ` (backquote), or << and >> (double angle
     1.5  brackets).
     1.6  
     1.7 +* More static checking of proof methods, which allows the system to
     1.8 +form a closure over the concrete syntax.  Method arguments should be
     1.9 +processed in the original proof context as far as possible, before
    1.10 +operating on the goal state.  In any case, the standard discipline for
    1.11 +subgoal-addressing needs to be observed: no subgoals or a subgoal
    1.12 +number that is out of range produces an empty result sequence, not an
    1.13 +exception.  Potential INCOMPATIBILITY for non-conformant tactical
    1.14 +proof tools.
    1.15 +
    1.16  
    1.17  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.18