diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 14:09:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 14:09:50 +0000 |
| commit | e22511b7890c0653e67604d444df5574f9b3add2 (patch) | |
| tree | 668aa0bd6fb2fc171614deed9fa0349abad5bc30 /CHANGES | |
| parent | 6df08b4dfd7b462e3c62eea3bc2efb2b79649949 (diff) | |
Updated
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 12 |
1 files changed, 12 insertions, 0 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. + |