diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-15 18:37:32 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-15 18:37:32 +0000 |
| commit | d624e436a4d860e51cd84676bcbe22919b7885fe (patch) | |
| tree | b1564516dc2d0e22c23a4928d1b6f8f025ecc700 /lego/example.l | |
| parent | 09906b09bdb6fe2929d7f63b42381f423824fcc9 (diff) | |
Use infixes to show off X-Symbol
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 e5e6d7b8..535d5712 100644 --- a/lego/example.l +++ b/lego/example.l @@ -6,7 +6,7 @@ Module example Import lib_logic; -Goal {A,B:Prop}(and A B) -> (and B A); +Goal {A,B:Prop}(A /\ B) -> (B /\ A); intros; Refine H; intros; |