diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-06 16:33:59 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-06 16:33:59 +0000 |
| commit | eb2fb1dab704ee39fe81ab46a120f53622888ef3 (patch) | |
| tree | 8b6d336c964d33bbbb1ee1cd88933389fde9f296 /ccc | |
| parent | 0e9241e75ed1082ae2397a198c4b8b8101fff54d (diff) | |
Fix README
Diffstat (limited to 'ccc')
| -rw-r--r-- | ccc/README | 61 |
1 files changed, 9 insertions, 52 deletions
@@ -1,55 +1,12 @@ -Example Proof General instance for Isabelle +Proof General for the Casl Consistency Checker -Written by David Aspinall. +Author: Christoph Lüth <cxl@informatik.uni-bremen.de> + +This is a fairly straightforward instantiation of Proof General for +the Casl Consistency Checker, CCC. -Status: supported as a demonstration only - -======================================== - - - "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. - - - -======================================== - -README,v 7.0 2002/08/29 09:12:10 da Exp +CASL is the standard algebraic specification language, and CCC is a +tool to check consistency of CASL specifications. +For more information, hasten thee browser yonder: + http://www.informatik.uni-bremen.de/cofi/ccc |