diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-09-08 15:34:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-09-08 15:34:31 +0000 |
| commit | 9080a41cf03b726ff9da2a3ac15e4c6155dd0749 (patch) | |
| tree | 0f6a3941b6643c2adc0b6a888158ee71fc8a2ef7 /lego/example.l | |
| parent | 052e952796e8e1f0bdedc1b95522e4494cfa186e (diff) | |
Example copied from texinfo manual
Diffstat (limited to 'lego/example.l')
| -rw-r--r-- | lego/example.l | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/lego/example.l b/lego/example.l index c82e7b2c..b7a952d1 100644 --- a/lego/example.l +++ b/lego/example.l @@ -1,2 +1,7 @@ +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; +Save and_commutes; + -INSERT HANDY LEGO EXAMPLE HERE!
\ No newline at end of file |