Clean whitespace

1 files changed, 31 insertions, 31 deletions

diff --git a/hol98/hol98.el b/hol98/hol98.el
index 653bbcb8..57172649 100644
--- a/hol98/hol98.el
+++ b/hol98/hol98.el
@@ -1,6 +1,6 @@
 ;; hol98.el   Basic Proof General instance for HOL 98
 ;;
-;; Copyright (C) 2000 LFCS Edinburgh. 
+;; Copyright (C) 2000 LFCS Edinburgh.
 ;;
 ;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -14,7 +14,7 @@
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
-(proof-easy-config  'hol98 "HOL" 
+(proof-easy-config  'hol98 "HOL"
  proof-prog-name		 "hol.unquote"
  proof-terminal-char             ?\;
  proof-script-comment-start             "(*"
@@ -34,26 +34,26 @@
  proof-shell-cd-cmd              "FileSys.chDir \"%s\""
  proof-shell-filename-escapes    '(("\\\\" . "\\\\") ("\""   . "\\\""))
  proof-shell-interrupt-regexp    "Interrupted"
- proof-shell-start-goals-regexp  
- (proof-regexp-alt "Proof manager status" 
-		   "OK.." 
+ proof-shell-start-goals-regexp
+ (proof-regexp-alt "Proof manager status"
+		   "OK.."
 		   "val it =\n")
- proof-shell-end-goals-regexp    
+ proof-shell-end-goals-regexp
  (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack"
 		   "^[ \t]*: GoalstackPure.proofs")
  proof-shell-quit-cmd            "quit();"
- proof-assistant-home-page       
+ proof-assistant-home-page
  "http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html"
- proof-shell-annotated-prompt-regexp 
+ proof-shell-annotated-prompt-regexp
  "^- "
  ;; This one is nice but less reliable, I think.
  ;; "\\(> val it = () : unit\n\\)?- "
  proof-shell-error-regexp "^! "
- proof-shell-init-cmd		  
+ proof-shell-init-cmd
  "Help.displayLines:=3000;
   fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));
   fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;"
- ;; FIXME: add optional help topic parameter to help command. 
+ ;; FIXME: add optional help topic parameter to help command.
  proof-info-command		    "help \"hol\""
  proof-shell-proof-completed-regexp "Initial goal proved"
  ;; FIXME: next one needs setting so that "urgent" messages are displayed
@@ -67,27 +67,27 @@
  ;; (on Linux, presumably on Solaris too).
  proof-shell-process-connection-type t
 
- ;; 
+ ;;
  ;; Syntax table entries for proof scripts
  ;;
  proof-script-syntax-table-entries
  '(?\` "\""
-   ?\$ "."   
-   ?\/ "."   
-   ?\\ "."   
-   ?+  "."   
-   ?-  "."   
-   ?=  "."   
-   ?%  "."   
-   ?<  "."   
-   ?>  "."   
-   ?\& "."   
-   ?.  "w"   
-   ?_  "w"   
-   ?\' "w"   
-   ?\| "."   
+   ?\$ "."
+   ?\/ "."
+   ?\\ "."
+   ?+  "."
+   ?-  "."
+   ?=  "."
+   ?%  "."
+   ?<  "."
+   ?>  "."
+   ?\& "."
+   ?.  "w"
+   ?_  "w"
+   ?\' "w"
+   ?\| "."
    ?\* ". 23"
-   ?\( "()1" 
+   ?\( "()1"
    ?\) ")(4")
 
  ;;
@@ -104,11 +104,11 @@
 		   "Induct" "Cases" "Cases_on" "Induct_on"
 		   "std_ss" "arith_ss" "list_ss"
 		   "define_type")
- hol98-rules	 '("ASSUME" "REFL" "BETA_CONV" "SUBST" 
+ hol98-rules	 '("ASSUME" "REFL" "BETA_CONV" "SUBST"
 		   "ABS" "INST_TYPE" "DISCH" "MP"
 		   "T_DEF" "FORALL_DEF" "AND_DEF" "OR_DEF" "F_DEF"
 		   "NOT_DEF" "EXISTS_UNIQUE_DEF" "BOOL_CASES_AX"
-		   "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF" 
+		   "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF"
 		   "ONTO_DEF" "INFINITY_AX" "LET_DEF" "COND_DEF" "ARB_DEF")
  hol98-tactics   '("ACCEPT_TAC" "ASSUME_TAC" "GEN_TAC"
 		   "CONJ_TAC" "DISCH_TAC" "STRIP_TAC"
@@ -122,7 +122,7 @@
  hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN"
 		   "THENL" "EVERY" "REPEAT"
 		   "MAP_EVERY")
- proof-script-font-lock-keywords	
+ proof-script-font-lock-keywords
  (list
   (cons (proof-ids-to-regexp hol98-keywords) 'font-lock-keyword-face)
   (cons (proof-ids-to-regexp hol98-tactics) 'font-lock-keyword-face)
@@ -134,7 +134,7 @@
  ;;
  proof-goals-font-lock-keywords
  (list
-  (cons (proof-ids-to-regexp '("Proof manager status" 
+  (cons (proof-ids-to-regexp '("Proof manager status"
 			       "proof" "Incomplete"
 			       "Initial goal proved"
 			       "Initial goal"
@@ -147,7 +147,7 @@
   (cons ": GoalstackPure.proofs"    'proof-boring-face)
   (cons ": Thm.thm"		    'proof-boring-face)
   (cons "val it ="		    'proof-boring-face))
- 
+
  ;; End of easy config.
  )