Update for current Coq syntax

1 files changed, 29 insertions, 28 deletions

diff --git a/etc/coq/naming.v b/etc/coq/naming.v
index ee078a60..53455239 100644
--- a/etc/coq/naming.v
+++ b/etc/coq/naming.v
@@ -1,49 +1,50 @@
 (* Coq theorems, etc can be named at the top .... *)
 
-Theorem and_comms: (A,B:Prop)(A /\ B) -> (B /\ A).
-  Intros A B H.
-  Induction H.
-  Apply conj.
-  Assumption.
-  Assumption.
+Theorem and_comms: forall (A B:Prop),(A /\ B) -> (B /\ A). 
+  intros A B H.
+  induction H.
+  apply conj.
+  assumption.
+  assumption.
 Qed.
 
 (* at the bottom... *)
 
-Goal (A,B:Prop)(A /\ B) -> (B /\ A).
-  Intros A B H.
-  Induction H.
-  Apply conj.
-  Assumption.
-  Assumption.
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A). 
+  intros A B H.
+  induction H.
+  apply conj.
+  assumption.
+  assumption.
 Save and_comms2.
 
 (* or not at all! *)
 (* 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)(A /\ B) -> (B /\ A).
-  Intros A B H.
-  Induction H.
-  Apply conj.
-  Assumption.
-  Assumption.
+Goal forall (A B:Prop),(A /\ B) -> (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! *)
+(* Odd side effect: two unnamed theorems in a row are not possible! 
+   Latest: with Coq 8.2, we get Unamed_thm0, Unamed_thm1, ... *)
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A). 
+  intros A B H.
+  induction H.
+  apply conj.
+  assumption.
+  assumption.
+Save.
 
 (* TESTING: notice output window behaviour here with different settings:
    exact output displayed also depends on how many steps are issued
    at once.
 *)
 
-Goal (A,B:Prop)(and A B) -> (and B A).
-Intros A B H.
-Induction H.
-Apply conj.
-Assumption.
-Assumption.
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A). 
+tauto.
 Save.   
-
-
-