diff options
| -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. - - - |