diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-06 16:18:57 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-06 16:18:57 +0000 |
| commit | 5f2e909816303f19e26b074e27ee2a2bd5bc11f8 (patch) | |
| tree | ce813bdca7110b786c3517879105d1c7caa15a26 /lego/example.l | |
| parent | 612d4dc6a021662d85d5a0ced9b17d1cb0c8cd2d (diff) | |
new maintainer for LEGO Proof General
Diffstat (limited to 'lego/example.l')
| -rw-r--r-- | lego/example.l | 5 |
1 files changed, 3 insertions, 2 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; |