diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-09-24 15:48:28 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-09-24 15:48:28 +0000 |
| commit | 6189e10da761f1d63135efa068cc428454e069f2 (patch) | |
| tree | df8565297bd056f71ed1e433acb92f32e90c8fad /lego/example.l | |
| parent | dde2904045d871721d4e015911199b24e14cd7a3 (diff) | |
unified example with other proof assistants;
Diffstat (limited to 'lego/example.l')
| -rw-r--r-- | lego/example.l | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/lego/example.l b/lego/example.l index 4a506990..e5e6d7b8 100644 --- a/lego/example.l +++ b/lego/example.l @@ -6,9 +6,10 @@ Module example 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; - - +Goal {A,B:Prop}(and A B) -> (and B A); +intros; +Refine H; +intros; +andI; +Immed; +Save and_comms; |