diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-12-15 18:01:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-15 18:01:31 +0000 |
| commit | f92abf977ec1decb12d82ef25c3c288e8689e4bb (patch) | |
| tree | bc572a5e7e786905097f2b5c5ee7cb8b2698835a | |
| parent | f990f85aa91bf15a3f93c8237e5efbf185ec5a46 (diff) | |
Preface: Added David von Oheimb to credits. Mentioned adding multiple files.
| -rw-r--r-- | doc/ProofGeneral.texi | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index f1b0ac37..3a29a21d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -310,7 +310,8 @@ Pascal Brisset, Rod Burstall, Paul Callaghan, Martin Hofmann, -James McKinna, +James McKinna, +David von Oheimb, and Markus Wenzel. Thanks to all of you! @@ -367,13 +368,15 @@ instantiation for Isabelle. Actually, our previous version wasn't quite as generic as we had hoped. Whereas LEGO and Coq are similar systems in many ways, Isabelle was really a different beast. Fierce reengineering and various improvements were provided by David Aspinall and Thomas -Kleymann to really make the code generic. - -It was time to come up with a -better name than just @code{proof} mode. David Aspinall suggested -@emph{Proof General}. He also cooked up some images and a toolbar. Proof -General 2.0 is the first official release, ready to conquer the world. -Why not adapt Proof General to your favourite proof system? +Kleymann to make it easier to instantiate to new proof systems. The +major technical improvement was the extension of script management to +work across multiple files. + +It was time to come up with a better name than just @code{proof} +mode. David Aspinall suggested @emph{Proof General}. He also cooked up +some images and a toolbar. Proof General 2.0 is the first official +release, ready to conquer the world. Why not adapt Proof General to +your favourite proof system? |