diff options
-rw-r--r-- | lego/example.l | 5 | ||||
-rw-r--r-- | lego/lego-syntax.el | 4 | ||||
-rw-r--r-- | lego/lego.el | 4 |
3 files changed, 6 insertions, 7 deletions
diff --git a/lego/example.l b/lego/example.l index b7a952d1..a15ea588 100644 --- a/lego/example.l +++ b/lego/example.l @@ -1,7 +1,8 @@ Module Walkthrough Import lib_logic; + Goal and_commutes: {A,B:Prop}(and A B) -> (and B A); -intros;andI; -Refine H;intros;Immed;Refine H;intros; Immed; +intros; andI; +Refine H; intros; Immed; Refine H; intros; Immed; Save and_commutes; diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 64399546..a49ee574 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -1,8 +1,8 @@ ;; lego-syntax.el Syntax of LEGO ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Author: Thomas Kleymann and Dilip Sequeira -;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; Please let us know if you could maintain this package! +;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> + ;; ;; $Id$ ;; diff --git a/lego/lego.el b/lego/lego.el index 04f02224..8fd09c64 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -1,9 +1,7 @@ ;; lego.el Major mode for LEGO proof assistants ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Author: Thomas Kleymann and Dilip Sequeira -;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; Please let us know if you could maintain this package! - +;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> ;; ;; $Id$ |