diff options
| author | David Aspinall | 2000-12-14 18:53:29 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-12-14 18:53:29 +0000 |
| commit | 4afd3c45883bd424028ef8dd341d34cf2df8f1e3 (patch) | |
| tree | ca559be0c36282f98d52b618ce761ef058c53a37 /etc/coq/multiple/c.v | |
| parent | 2ce3be2f0405b9e8f86f0b6e335ecd8bcdc40312 (diff) | |
Updated to use Require commands
Diffstat (limited to 'etc/coq/multiple/c.v')
| -rw-r--r-- | etc/coq/multiple/c.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/etc/coq/multiple/c.v b/etc/coq/multiple/c.v index ffdf1d5e..490c3250 100644 --- a/etc/coq/multiple/c.v +++ b/etc/coq/multiple/c.v @@ -1,4 +1,7 @@ -(* Silly tests for automatic auto file handling *) +(* Simple tests for multiple file handling *) + +Require a. +Require b. Goal (A,B:Prop)(and A B) -> (and B A). Intros A B H. |