aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1999-11-15 18:37:32 +0000
committerDavid Aspinall1999-11-15 18:37:32 +0000
commitd624e436a4d860e51cd84676bcbe22919b7885fe (patch)
treeb1564516dc2d0e22c23a4928d1b6f8f025ecc700
parent09906b09bdb6fe2929d7f63b42381f423824fcc9 (diff)
Use infixes to show off X-Symbol
-rw-r--r--lego/example.l2
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;