From b35ce5388cfbd86b2be92e7acb56ff4aa215f58a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 5 Sep 2009 10:42:23 +0000 Subject: Clean whitespace --- lego/lego-syntax.el | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'lego') diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 5cf7867a..44a17ade 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -1,5 +1,5 @@ ;; lego-syntax.el Syntax of LEGO -;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Author: Thomas Kleymann and Dilip Sequeira ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Paul Callaghan @@ -22,8 +22,8 @@ "Cut" "Discharge" "DischargeKeep" "echo" "exE" "exI" "Expand" "ExpAll" "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" - "impE" "impI" "Induction" "Inductive" - "Invert" "Init" "intros" "Intros" "Module" "Next" + "impE" "impI" "Induction" "Inductive" + "Invert" "Init" "intros" "Intros" "Module" "Next" "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) "Subset of LEGO keywords and tacticals which are terminated by a \?;") @@ -37,7 +37,7 @@ ;; ----- regular expressions for font-lock (defconst lego-error-regexp "^\\(cannot assume\\|Error\\|Lego parser\\)" - "A regular expression indicating that the LEGO process has identified an error.") + "A regular expression indicating that the LEGO process has identified an error.") (defvar lego-id proof-id) @@ -74,7 +74,7 @@ ; Pi and Sigma binders (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 'proof-declaration-name-face) - + ;; Kinds (cons (concat "\\\\|\\