diff options
| author | Thomas Kleymann | 1998-07-27 15:39:57 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-07-27 15:39:57 +0000 |
| commit | e1b55f8f678058f30fd22317b5215d539b836aa9 (patch) | |
| tree | 4d8e3944e456c7fd155e57dc26e7b7611beb77c7 | |
| parent | 90fa6289aff871fc53d646af37894b0ad658cd34 (diff) | |
Supports official LEGO release 1.3
| -rw-r--r-- | lego-fontlock.el | 5 | ||||
| -rw-r--r-- | lego.el | 5 | ||||
| -rw-r--r-- | script-management.texinfo | 2 |
3 files changed, 9 insertions, 3 deletions
diff --git a/lego-fontlock.el b/lego-fontlock.el index 289d8328..437c4906 100644 --- a/lego-fontlock.el +++ b/lego-fontlock.el @@ -6,6 +6,9 @@ ;; should perhaps be called lego-syntax instead of lego-fontlock ;; $Log$ +;; Revision 1.6 1998/07/27 15:39:53 tms +;; Supports official LEGO release 1.3 +;; ;; Revision 1.5 1998/05/29 09:49:40 tms ;; o outsourced indentation to proof-indent ;; o support indentation of commands @@ -49,7 +52,7 @@ "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" "impE" "impI" "Induction" "Inductive" "Invert" "Init" "intros" "Intros" "Module" "Next" - "Normal" "notE" "notI" "orE" "orIL" "orIR" "Qnify" + "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 \?;") @@ -5,6 +5,9 @@ ;; $Log$ +;; Revision 1.52 1998/07/27 15:39:56 tms +;; Supports official LEGO release 1.3 +;; ;; Revision 1.51 1998/06/10 11:43:38 hhg ;; Added lego-init-syntax-table as function to initialize syntax entries ;; particular to LEGO, and call it from lego-shell-mode-config. @@ -248,7 +251,7 @@ (defvar lego-undoable-commands-regexp (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal" "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption" - "UTac" "Qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI" + "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI" "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed" "Invert")) "Undoable list") diff --git a/script-management.texinfo b/script-management.texinfo index 71575d1f..3e07455b 100644 --- a/script-management.texinfo +++ b/script-management.texinfo @@ -15,7 +15,7 @@ @c The following two commands start the copyright page. @page @vskip 0pt plus 1filll -Copyright @copyright{} 1997 LEGO Team, LFCS Edinburgh +Copyright @copyright{} 1997, 1998 LEGO Team, LFCS Edinburgh @end titlepage @node Top, Introduction, (dir), (dir) |
