diff -r f90326b13080 -r a1b697a2f3a8 NEWS --- a/NEWS Wed Dec 23 17:24:12 2015 +0100 +++ b/NEWS Wed Dec 23 17:35:07 2015 +0100 @@ -628,6 +628,10 @@ *** ML *** +* Pretty printing of Poly/ML compiler output in Isabelle has been +improved: proper treatment of break offsets and blocks with consistent +breaks. + * Isar proof methods are based on a slightly more general type context_tactic, which allows to change the proof context dynamically (e.g. to update cases) and indicate explicit Seq.Error results. Former