From 3dff233bbf3e377e3d2dbf889f16560d0517de57 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 16 Nov 1999 16:01:36 +0000
Subject: Note about how to use demoisa and isar instances.  Other comments

---
 generic/proof-site.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'generic')

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.
-- 
cgit v1.2.3