From d624e436a4d860e51cd84676bcbe22919b7885fe Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 15 Nov 1999 18:37:32 +0000 Subject: Use infixes to show off X-Symbol --- lego/example.l | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lego/example.l') 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; -- cgit v1.2.3