diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 6 insertions, 1 deletions
@@ -76,9 +76,14 @@ Coq Changes Isabelle and Isar Changes ------------------------- -* Tweaks for input syntax. +* Several tweaks for input syntax. * Recognize goals of the old form val prems = goal ... + and saves of the old form val thm = result. + +* Proofs which are "unfinished", i.e. have no qed or result, + are now closed off automatically when a new goal is begun, + mirroring the behaviour of Isabelle. Only in the developers' release |