diff options
| author | David Aspinall | 1999-11-16 16:01:36 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-16 16:01:36 +0000 |
| commit | 3dff233bbf3e377e3d2dbf889f16560d0517de57 (patch) | |
| tree | 57062c98bac845f6fd605ed8fc362d3ba50839ff | |
| parent | b60783fa894f0956cb581c8f2aee1423faf12096 (diff) | |
Note about how to use demoisa and isar instances. Other comments
| -rw-r--r-- | generic/proof-site.el | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 2bb26e29..95475ae7 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -42,7 +42,7 @@ ;; Isabelle interfaces at the same time! (defcustom proof-assistant-table '(;; For demonstration instance of Proof General, - ;; set PROOFGENERAL_ASSISANTS=demoisa. It really works! + ;; set PROOFGENERAL_ASSISANTS=demoisa. ;; To use Isabelle/Isar instead of classic Isabelle, ;; set PROOFGENERAL_ASSISANTS=isar (demoisa "Isabelle Demo" "\\.ML$") @@ -254,6 +254,9 @@ Note: to change proof assistant, you must start a new Emacs session.") :prefix ,(concat sname "-")) ;; Set the proof-assistant configuration variables + ;; NB: tempting to use customize-set-variable: wrong! + ;; Here we treat customize as extended docs for these + ;; variables. (setq proof-assistant ,assistant-name) (setq proof-assistant-symbol (quote ,assistant)) ;; Extend the load path, load the real mode and invoke it. |