From 5a5c39dedd0f3491245d4cc1d156682e5b1fac91 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 16 Nov 1999 15:40:46 +0000 Subject: Spruced up features list --- html/features.phtml | 117 ++++++++++++++++++++++++++++++++-------------------- 1 file changed, 72 insertions(+), 45 deletions(-) (limited to 'html/features.phtml') diff --git a/html/features.phtml b/html/features.phtml index 4dc01cef..0b3fee7d 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -5,12 +5,27 @@ It doesn't matter if you're an Emacs militant or a pacifist!

-Proof General will be useful to you if you use a proof -assistant, and you'd like some of the following features: +Proof General is designed to be useful for novices and expert users alike. +
+It will be useful to you if you use a proof assistant, and +you'd like an interface with the following features: +script management, +multiple file scripting, +proof by pointing, +toolbar and menus, +syntax highlighting, +real symbols, +definitions menu, +tags, +and finally, +adaptability. +
+Are you convinced yet? +If not, read on…

- +
- +
A proof script is a sequence of commands sent to a proof assistant to construct a proof, usually stored in @@ -32,39 +47,33 @@ assistant, and you'd like some of the following features: of Proof General to see script managament in action.

- +
Script management in Proof General can work across many script - files. When a script is visited in the editor, it is - coloured to reflect whether the proof assistant has loaded it in - this session. + files. When a script is visited in the editor, it is locked + (coloured) to reflect whether the proof assistant has loaded it in + this session. When a file is unlocked, all of the files which + depend on it are automatically unlocked too.

- Dependencies between script files are - communicated from the proof assistant to Proof General. - If you want to edit a file which has been loaded into the - proof assistant already, Proof General will unlock the file - and all the files which depend on it. This connects the - editor with the theory dependency or make system of the - proof assistant. + Dependencies between script files are either communicated from the + proof assistant to Proof General, or maintained automatically by + Proof General (based on the order in which files were processed).

-
- +
Proof by pointing allows you to click on a subterm of a goal to be proved, and apply an appropriate rule or tactic automatically.

- Proof by pointing uses the - interface to highlight subterms under the mouse, and Proof General - uses the subterm structure to make it easy - to cut and paste complicated subterms. + Proof by pointing uses the interface to highlight subterms under the + mouse, and sends messages asking the prover for hints to proceed. + Proof General also uses the subterm structure to make it easy to cut + and paste from complicated terms.

- +
- +
Proof General has a toolbar with buttons for examining the proof state, starting a proof, manoeuvring in the proof script, @@ -73,10 +82,14 @@ assistant, and you'd like some of the following features:

Using the toolbar, you can replay proofs without knowing any low-level commands of the proof assistant or any Emacs hot-keys! +

+ Additionally, the toolbar commands and many more besides are + available on menus; you don't need to know magical key presses for + any features.

- +
Syntax highlighting is an editing feature which decorates a file with different colours or fonts according to the syntax of some @@ -87,19 +100,21 @@ assistant, and you'd like some of the following features: assumptions, for example.

- +
- Tags are an editing feature which allow you to quickly locate - the definition or declaration of a particular identifier. + Proof General has a close integration with the + powerful + X-Symbol + package, which makes it easy to transparently use real symbols and + Greek letters in your proofs. +
Instead of seeing "not P", you see "¬
P", instead + of "a * b", you see "a × b", etc.
+ [the examples above are simple so they will work on most browsers + without needing images]

- Proof General is supplied with utilities to make tag indexes - for Emacs. This makes it easy to quickly access definitions from a - standard library, for example, and in large proof developments - split across multiple files. - -

+ - +
A pull-down menu gives easy access to definitions, declarations and proofs in the current @@ -113,18 +128,31 @@ assistant, and you'd like some of the following features: remotely, while your files and editor reside on your local machine.

- +
- Proof General is designed to be generic, so you can adapt it - to a new proof assistant if you know a little bit of Emacs - Lisp. + Tags are an editing feature which allow you to quickly locate the + definition or declaration of a particular identifier. Proof General + is supplied with utilities to make tag indexes for Emacs, for the + proof assistants LEGO and Coq. This makes it easy to quickly access + definitions from a standard library, for example, and in large proof + developments split across multiple files. + +

+
+ +
+ Proof General is designed to be adaptable. Many aspects + of its behaviour can be easily customized (using dialogue boxes and + buttons, no text file editing!). +

+ Most importantly, Proof General is generic, so you can adapt it to + a new proof assistant with surprisingly little effort.

Adapting for a new proof assistant is mainly a matter of setting some variables with regular expressions to help parse output from the prover, and setting other variables with commands to send to the - prover. - To get the most from Proof General (proof-by-pointing, for example), - it may be necessary to augment the output routines of the + prover. To get the most from Proof General (proof by pointing, for + example), it may be necessary to augment the output routines of the proof assistant.

Please feel free to download Proof General to customize it for a new @@ -133,9 +161,8 @@ assistant, and you'd like some of the following features: how you get on.
-

-For more details of the above features, see the +For (even) more details of the above features, see the

-- cgit v1.2.3