diff options
| -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. |