diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-15 12:10:34 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-15 12:10:34 +0000 |
| commit | 3e9fc0816fc333ff80d158afa26bb70e403e6b1f (patch) | |
| tree | 3ff9aaf8a4ee303893428e8a22d9e064fceb525a /lego/example.l | |
| parent | e5a5aa225eb864da82c00870698d79befca977d8 (diff) | |
made many minor changes to the documentation
Diffstat (limited to 'lego/example.l')
| -rw-r--r-- | lego/example.l | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lego/example.l b/lego/example.l index a15ea588..52643424 100644 --- a/lego/example.l +++ b/lego/example.l @@ -1,4 +1,4 @@ -Module Walkthrough Import lib_logic; +Module example Import lib_logic; Goal and_commutes: {A,B:Prop}(and A B) -> (and B A); intros; andI; |