NEWS
changeset 61841 4d3527b94f2a
parent 61823 5daa82ba4078
child 61848 9250e546ab23
     1.1 --- a/NEWS	Sat Dec 12 15:37:42 2015 +0100
     1.2 +++ b/NEWS	Sun Dec 13 21:56:15 2015 +0100
     1.3 @@ -626,6 +626,12 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Isar proof methods are based on a slightly more general type
     1.8 +context_tactic, which allows to change the proof context dynamically
     1.9 +(e.g. to update cases) and indicate explicit Seq.Error results. Former
    1.10 +METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
    1.11 +provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
    1.12 +
    1.13  * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
    1.14  
    1.15  * The auxiliary module Pure/display.ML has been eliminated. Its