From a893053a2949e94d54eddb53aa31b61fb31b3679 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 17 Jan 2008 12:55:55 +0000
Subject: Fix included file

---
 doc/PG-adapting.texi | 15 +--------------
 1 file changed, 1 insertion(+), 14 deletions(-)

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index ac8ad8d4..ee3a75c7 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3932,7 +3932,7 @@ Proof General.
 
 @lisp
 @c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM
-@c @includeverbatim ../demoisa/demoisa-easy.el
+@c @includeverbatim ../demoisa/demoisa.el
 ;; demoisa.el Example Proof General instance for Isabelle
 ;;
 ;; Copyright (C) 1999 LFCS Edinburgh. 
@@ -4076,19 +4076,6 @@ Proof General.
 ;; add highlighting, or some of the proof by pointing markup
 ;; configuration for the goals buffer.
 
-;; The final piece of magic here is a hook which configures settings
-;; to get the proof shell running.  Proof General needs to know the
-;; name of the program to run, and the modes for the shell, response,
-;; and goals buffers.
-
-(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start)
-
-(defun demoisa-pre-shell-start ()
-  (setq proof-prog-name		isabelledemo-prog-name)
-  (setq proof-mode-for-shell    'demoisa-shell-mode)
-  (setq proof-mode-for-response 'demoisa-response-mode)
-  (setq proof-mode-for-goals	'demoisa-goals-mode))
-
 (provide 'demoisa)
 @end lisp
 
-- 
cgit v1.2.3