Test for Unnamed_thm.

1 files changed, 30 insertions, 0 deletions

diff --git a/etc/coq/unnamed_thm.v b/etc/coq/unnamed_thm.v
new file mode 100644
index 00000000..2bd82b7b
--- /dev/null
+++ b/etc/coq/unnamed_thm.v
@@ -0,0 +1,30 @@
+(*
+    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.   
+
+
+