diff options
| -rw-r--r-- | CHANGES | 12 | ||||
| -rw-r--r-- | todo | 4 |
2 files changed, 14 insertions, 2 deletions
@@ -18,18 +18,30 @@ *** Added possibility for switching prover's output on/off. + Already implemented in Coq and Isabelle(/Isar). + ** Coq Changes +*** More decoration of Coq output, uses CoqResp mode now + ** LEGO Changes +*** Slight change in output during proof: show final discharge messages + ** Isabelle Changes *** Fix for stack overflow in regexp which occurred with large proof states ** Isar Changes +** HOL Changes + +*** Output decoration improvements. + ** Changes for developers to note *** No need for match string 1 in proof-shell-proof-completed +*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity. + @@ -29,7 +29,7 @@ X (Low) e.g. probably not worth spending time on *** Scheduled improvements for 3.2 -**** A Doc new bits: font lock keywords, silent stuff, filename %e, %r. +**** A Doc new bits: font lock keywords, filename %e, %r. **** A Add a new keymap(s) for proof assistants. Presently they naughtily bind C-c <letter> which are reserved for @@ -42,7 +42,7 @@ X (Low) e.g. probably not worth spending time on **** A Add efficiency improvement by turning on/off prover output. Patch already added to pre-release. - Needs adjusting to turn on output in case of error/interrupt. + Does it need adjusting to turn on output in case of error/interrupt? **** C Add improvements to script movement in electric terminator mode. Some commented regions in code. E.g. automatic newline/space after |