aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example.v
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-01-16 16:39:06 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-01-16 16:39:06 +0000
commite36ec50c0995858321748f5d4f7bd73472e2464d (patch)
tree32330abd62c6dcfe12eea510c4ad9ab9093f5790 /coq/example.v
parentb53246d8464ce383b4d607209b41bfdc8c966365 (diff)
Whitespace
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.