diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-05 15:09:21 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-05 15:09:21 +0000 |
| commit | 3d2978cf896be29b579cb56b6c33b867d093b587 (patch) | |
| tree | cdfc56743c5e0ea4649a200b9ee61fb8f9b8788a /CHANGES | |
| parent | 980ca5b3c0dc3e4bdbc7bd96e91071f8b10eb8d3 (diff) | |
Updated
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -15,6 +15,12 @@ *** Improved behaviour of electric terminator +*** Point never moves if proof-follow-mode is 'ignore. + + Previously it was always moved when an error occurred. + It's nicer to do this manually if you like this mode, + using M-x proof-goto-end-of-locked. + *** Efficiency improvement in parsing Also works around crash bug in xemacs-21.1.7/SuSE. @@ -37,10 +43,16 @@ ** Isabelle Changes +*** More code from Isamode has been merged into Proof General + + Particularly: the user now can choose a logic image from inside PG. + *** Fix for stack overflow in regexp which occurred with large proof states ** Isar Changes +*** Fix for stack overflow in regexp which occurred with large proof states + ** HOL Changes *** Output decoration improvements. |