From 153955899a42b9ef4c7ce5ad8cd9bcd82a39eb83 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 8 Sep 2009 23:17:33 +0000 Subject: Remove more of 80 code --- coq/example.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'coq/example.v') diff --git a/coq/example.v b/coq/example.v index f482f2ab..939f89c9 100644 --- a/coq/example.v +++ b/coq/example.v @@ -6,7 +6,7 @@ Module Example. -Goal forall (A B:Prop),(A /\ B) -> (B /\ A). +Goal forall (A B:Prop),(A /\ B) -> (B /\ A). intros A B. intros H. elim H. @@ -16,6 +16,3 @@ Goal forall (A B:Prop),(A /\ B) -> (B /\ A). Save and_comms. End Example. - - - -- cgit v1.2.3