From e40001d34fef5595487558f33e5a6a7cdadaec77 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 14 May 2013 19:28:23 +0000 Subject: - update coq example - minor changes in user manual --- 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 5c6894c7..27ccd26d 100644 --- a/coq/example.v +++ b/coq/example.v @@ -6,13 +6,13 @@ Module Example. -Goal forall (A B:Prop),(A /\ B) -> (B /\ A). - intros A B. - intros H. - elim H. - split. - assumption. - assumption. -Save and_comms. + Lemma and_commutative : forall (A B:Prop),(A /\ B) -> (B /\ A). + Proof. + intros A B H. + destruct H. + split. + trivial. + trivial. + Qed. End Example. -- cgit v1.2.3