aboutsummaryrefslogtreecommitdiffhomepage
path: root/demoisa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-05 10:42:23 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-05 10:42:23 +0000
commitb35ce5388cfbd86b2be92e7acb56ff4aa215f58a (patch)
treeaa6f57349bb07993bf80136e6dd18a8fe0e6ea84 /demoisa
parent41a4f20e3250cbe225fb8363738a6c6ac35d0368 (diff)
Clean whitespace
Diffstat (limited to 'demoisa')
-rw-r--r--demoisa/demoisa.el10
1 files changed, 5 insertions, 5 deletions
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 70886a85..45c712e7 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -1,6 +1,6 @@
;; demoisa.el Example Proof General instance for Isabelle
;;
-;; Copyright (C) 1999 LFCS Edinburgh.
+;; Copyright (C) 1999 LFCS Edinburgh.
;;
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;;
@@ -19,8 +19,8 @@
;;
;; From this it loads this file "demoisa/demoisa.el" whenever
;; a .ML file is visited, and sets the mode to `demoisa-mode'
-;; (defined below).
-;;
+;; (defined below).
+;;
;; I've called this instance "Isabelle Demo Proof General" just to
;; avoid confusion with the real "Isabelle Proof General" in case the
;; demo gets loaded by accident.
@@ -46,7 +46,7 @@
;; (constants, but may be nice to tweak)
;;
;; The first group appears in the menu
-;; ProofGeneral -> Customize -> Isabelledemo
+;; ProofGeneral -> Customize -> Isabelledemo
;; The second group appears in the menu:
;; ProofGeneral -> Internals -> Isabelledemo config
;;
@@ -100,7 +100,7 @@
proof-shell-proof-completed-regexp "^No subgoals!"
proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading"
proof-shell-init-cmd ; define a utility function, in a lib somewhere?
- "fun pg_repeat f 0 = ()
+ "fun pg_repeat f 0 = ()
| pg_repeat f n = (f(); pg_repeat f (n-1));"
proof-shell-quit-cmd "quit();"))