From 1aaf83d4ce7ff643de45e85bf7f5a6bebaa8c38a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 21 Apr 2004 22:22:13 +0000 Subject: Update for V8 syntax. --- coq/example.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'coq/example.v') diff --git a/coq/example.v b/coq/example.v index cfe85203..6e88c5c8 100644 --- a/coq/example.v +++ b/coq/example.v @@ -1,14 +1,14 @@ (* - Example proof script for Coq Proof General. + Example proof script for Coq Proof General (Coq V8 syntax). $Id$ *) -Goal (A,B:Prop)(A /\ B) -> (B /\ A). - Intros A B H. - Elim H. - Intros. - Split. - Assumption. - Assumption. +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). + intros A B H. + elim H. + intros. + split. + assumption. + assumption. Save and_comms. -- cgit v1.2.3