diff options
| author | David Aspinall | 1999-11-17 19:55:59 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-17 19:55:59 +0000 |
| commit | 9b8e1d43f08282a824c4c8db782593475411d791 (patch) | |
| tree | 40df206376226fd2d2a87bf3112db36445e275f2 | |
| parent | 8c2a3169e10622db9ae0c595174b78f57a665286 (diff) | |
Deleted files.
| -rw-r--r-- | etc/mailinglist-bait | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/etc/mailinglist-bait b/etc/mailinglist-bait deleted file mode 100644 index 6fa15b9c..00000000 --- a/etc/mailinglist-bait +++ /dev/null @@ -1,34 +0,0 @@ -Dear Proof General users, - -This is a newsy note to tell you that Proof General 3.0 is ready for -release Very Soon Now. In the meantime, I'd be very grateful to -anyone who can test a pre-release and tell me how it goes. - -I'm quite excited about this release. I've concentrated on usability, -making the code clean and robust, and making PG easier to adapt for -new proof assistants. But there are some important new features too... - -David von Oheimb's patches for X-Symbol have been made a proper -generic part of Proof General now, and easy to turn on and off. -I've added some basic support for Coq and LEGO, so Greek letters and -symbols like /\ and -> display as you would like. Break free -from ASCII! - -Proof-by-pointing has been resurrected. The interface relies on the -proof assistant to construct the proof commands, and the only prover -supported currently is LEGO. One reason PBP was disabled was that -LEGO's implementation is experimental and incomplete. But I hope that -people can see PBP almost working in LEGO and be encouraged to -implement it for other provers. We can certainly hope for support in -Coq, since the CtCoq proof-by-pointing code has been moved into the -Coq kernel now. I hope the Coq community can encourage somebody to do -this. - -Visit http://zermelo.dcs.ed.ac.uk/~proofgen/ for more. - -Best regards, - - - David. - - - |