| changeset 61922 | a1b697a2f3a8 |
| parent 61907 | f0c894ab18c9 |
| child 61941 | 31f2105521ee |
--- 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