From 1c176fd06d7345e58ec5636cf9fbec4dd8fdda8f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Jan 2015 10:42:39 -0800 Subject: [PATCH] feat(doc/bin/README): add link to documentation --- doc/bin/README.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/doc/bin/README.md b/doc/bin/README.md index 37ac2c58e..46e32f813 100644 --- a/doc/bin/README.md +++ b/doc/bin/README.md @@ -16,6 +16,15 @@ the following command executes a simple set of examples The Emacs mode is the ideal way to use Lean. It requires at least Emacs version 24.3 +Documentation +------------- + +The tutorial "Theorem Proving in Lean" describes Lean main features, +and provides many examples. The tutorial is available in two different forms: + + - Interactive HTML: http://leanprover.github.io/tutorial/index.html + - PDF: http://leanprover.github.io/tutorial/tutorial.pdf + Command line options --------------------