aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example.v
diff options
context:
space:
mode:
Diffstat (limited to 'coq/example.v')
-rw-r--r--coq/example.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/coq/example.v b/coq/example.v
index 010248a6..5a3c5b59 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -4,7 +4,6 @@
$Id$
*)
-
Goal (A,B:Prop)(A /\ B) -> (B /\ A).
Intros A B H.
Induction H.