From 948b8bd7a59b7c35552cb0f4a5b95ee8574f5686 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 13 Nov 1999 13:53:35 +0000
Subject: Use infix syntax

---
 coq/example.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq/example.v b/coq/example.v
index 4fb38af6..1155e5f7 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -4,7 +4,8 @@
     $Id$
 *)
 
-Goal (A,B:Prop)(and A B) -> (and B A).
+
+Goal (A,B:Prop)(A /\ B) -> (B /\ A).
 Intros A B H.
 Induction H.
 Apply conj.
@@ -12,4 +13,3 @@ Assumption.
 Assumption.
 Save and_comms.
 
-
-- 
cgit v1.2.3