aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThomas Kleymann1998-07-27 15:39:57 +0000
committerThomas Kleymann1998-07-27 15:39:57 +0000
commite1b55f8f678058f30fd22317b5215d539b836aa9 (patch)
tree4d8e3944e456c7fd155e57dc26e7b7611beb77c7
parent90fa6289aff871fc53d646af37894b0ad658cd34 (diff)
Supports official LEGO release 1.3
-rw-r--r--lego-fontlock.el5
-rw-r--r--lego.el5
-rw-r--r--script-management.texinfo2
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 \?;")
diff --git a/lego.el b/lego.el
index be7f1018..d0059f55 100644
--- a/lego.el
+++ b/lego.el
@@ -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)