diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 15:09:11 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 15:09:11 +0000 |
| commit | 8e5bbac00d44280363aa7cb63d536fddf6b24eee (patch) | |
| tree | 29f5f43b8a65f541026a407d1626ae037c1a4cb2 | |
| parent | 7fe13eaa8a9c26460db874eac8445e87ef1b4efa (diff) | |
Renamed from demoisa/README to obsolete/demoisa/README
| -rw-r--r-- | demoisa/README | 55 |
1 files changed, 0 insertions, 55 deletions
diff --git a/demoisa/README b/demoisa/README deleted file mode 100644 index 74b4d8d7..00000000 --- a/demoisa/README +++ /dev/null @@ -1,55 +0,0 @@ -Example Proof General instance for Isabelle - -Written by David Aspinall. - -Status: demonstration, only works for obsolete Isabelle versions - -======================================== - - - "Isabelle Proof General in 30 setqs" - -This is a whittled down version of Isabelle Proof General, supplied as -an (almost) minimal demonstration of how to instantiate Proof General -to a particular proof assistant. You can use this as a template to -get support for a new assistant going. (I did for HOL Proof General). - -This mode uses the unadulterated terminal interface of Isabelle, to -demonstrate that hacking the proof assistant is not necessary to get -basic features working. - -And it really works! You you get a toolbar, menus, short-cut keys, -script management for multiple files, a function menu, ability to -run proof assistant remotely, etc, etc. - -To try it out, set in the shell PROOFGENERAL_ASSISTANTS=demoisa -before invoking Emacs. (Of course, you need Isabelle installed). - -What's missing? - - 1. A few handy commands (e.g. proof-find-theorems-command) - 2. Syntax settings and highlighting for proof scripts - 3. Indentation for proof scripts - 4. Special markup characters in output for robustness - 5. True script management for multiple files (automatic mode is used) - 6. Proof by pointing - -How easy is it to add all that? - - 1. Trivial. 2. A table specifying syntax codes for characters - (strings, brackets, etc) and some regexps; depends on complexity - of syntax. 3. A bit of elisp to scan script; depends on - complexity of syntax. 4. Needs hacking in the proof assistant: - how hard is to hack your assistant to do this? 5. Depends on file - management mechanism in the prover, may need hacking there to send - messages. But automatic multiple files may be all you need anyway. - 6. Non trivial (but worth a go). - -See demoisa.el and demoisa-easy.el for more details. - - - -======================================== - -$Id$ - |