diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 23:17:33 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 23:17:33 +0000 |
| commit | 153955899a42b9ef4c7ce5ad8cd9bcd82a39eb83 (patch) | |
| tree | b77aa3fac8a901c6f60e6c5af793567d477d1d1e /coq/example.v | |
| parent | 9d866b03a550f72f3ad7f148e443c73f5fb03b73 (diff) | |
Remove more of 80 code
Diffstat (limited to 'coq/example.v')
| -rw-r--r-- | coq/example.v | 5 |
1 files changed, 1 insertions, 4 deletions
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. - - - |