diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-12-14 15:37:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-14 15:37:12 +0000 |
| commit | e5a5aa225eb864da82c00870698d79befca977d8 (patch) | |
| tree | 67a5a5d8bd26a160814184bab35400766934956a /etc | |
| parent | 89f4ac8070b2b7505dde4be775f764493af3bea3 (diff) | |
Altered order of new para and removed some mailing list addrs
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/announce | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/etc/announce b/etc/announce index 5b64d87b..1282a024 100644 --- a/etc/announce +++ b/etc/announce @@ -5,10 +5,8 @@ To: coq-club@pauillac.inria.fr, uitp@dcs.gla.ac.uk, bra-types@cs.chalmers.se, info-hol@leopard.cs.byu.edu, - protagonist@cs.kun.nl, ??? pvs@csl.sri.com, qed@mcs.anl.gov, - softverf@leopard.cs.byu.edu, ??? theorem-provers@ai.mit.edu, types@cs.indiana.edu, formal-methods@cs.uidaho.edu, @@ -113,17 +111,15 @@ Proof General provides a unified interface to different theorem provers. The advantage is that a novice who understands the Proof General interface can inspect and replay proofs in any of the theorem provers supported, without knowing the specific commands needed to -drive them. An obvious avenue towards further and easier unification -would be to invent a unified proof script (input) language and -proof-state (output) language for theorem provers. The Proof General -experience could provide useful insight into such a project. We'd be -interested to hear from workers interested in collaborating in this -area. - -Moreover, by implementing your user-interface ideas in the Proof -General framework, your contributions automatically reach a large -community of both novice and expert proof assistant users. - +drive them. Moreover, by implementing your user-interface ideas in +the Proof General framework, your contributions automatically reach a +large community of both novice and expert proof assistant users. + +An obvious avenue towards further and easier unification would be to +invent a unified proof script (input) language and proof-state +(output) language for theorem provers. The Proof General experience +could provide useful insight into such a project. We'd be interested +to hear from workers interested in collaborating in this area. -- David Aspinall & Thomas Kleymann (Please contact via proofgen@dcs.ed.ac.uk) |