diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 15:07:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 15:07:23 +0000 |
| commit | 2485896dae1ef3bbd5a8f83fc16f91c0adf4a22c (patch) | |
| tree | 910ddafc6041818a2444f5c85301b3d1ef6bcf6b /etc/coq | |
| parent | 348a98f9572bf54a9ee97e543cb9a0f07c6a5cc4 (diff) | |
Deleted files.
Diffstat (limited to 'etc/coq')
| -rw-r--r-- | etc/coq/unnamed_thm.v | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/etc/coq/unnamed_thm.v b/etc/coq/unnamed_thm.v deleted file mode 100644 index 2bd82b7b..00000000 --- a/etc/coq/unnamed_thm.v +++ /dev/null @@ -1,30 +0,0 @@ -(* - Test for Unnamed_thm - - $Id$ -*) - -(* Coq calls this "Unamed_thm", so must forget it like any other *) - -(* test: do, undo, then check shell buffer to see "Reset Unnamed_thm" *) - -Goal (A,B:Prop)(and A B) -> (and B A). -Intros A B H. -Induction H. -Apply conj. -Assumption. -Assumption. -Save. - -(* Odd side effect: two unnamed theorems in a row are not possible! *) - -Goal (A,B:Prop)(and A B) -> (and B A). -Intros A B H. -Induction H. -Apply conj. -Assumption. -Assumption. -Save. - - - |