1 files changed, 14 insertions, 0 deletions
diff --git a/coq/example.v b/coq/example.v
new file mode 100644
index 00000000..5a3c5b59
--- /dev/null
+++ b/coq/example.v
@@ -0,0 +1,14 @@
+(*
+    Example proof script for Coq Proof General.
+ 
+    $Id$
+*)
+
+Goal (A,B:Prop)(A /\ B) -> (B /\ A).
+  Intros A B H.
+  Induction H.
+  Apply conj.
+  Assumption.
+  Assumption.
+Save and_comms.
+