diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-21 22:22:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-21 22:22:13 +0000 |
| commit | 1aaf83d4ce7ff643de45e85bf7f5a6bebaa8c38a (patch) | |
| tree | b810f2bcb3dbbd4072b1c4b8d759dcc47be1512a /coq/example.v | |
| parent | 0baa4761f4482643c2368365ea679663313ae59e (diff) | |
Update for V8 syntax.
Diffstat (limited to 'coq/example.v')
| -rw-r--r-- | coq/example.v | 16 |
1 files changed, 8 insertions, 8 deletions
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. |