diff --git a/doc/bin/README.md b/doc/bin/README.md
new file mode 100644
index 000000000..37ac2c58e
--- /dev/null
+++ b/doc/bin/README.md
@@ -0,0 +1,42 @@
+Lean binary distribution
+------------------------
+
+The binary distribution package contains:
+
+- Lean executable (located in the sub-directory bin)
+- Standard library (located in the sub-directory lib/lean/library)
+- HoTT library (located in the sub-directory lib/lean/hott)
+- Emacs modes (located in the sub-directory share/emacs/site-list/lean)
+
+Assuming you are in the same directory this file is located,
+the following command executes a simple set of examples
+
+% bin/lean examples/ex.lean
+
+The Emacs mode is the ideal way to use Lean. It requires at
+least Emacs version 24.3
+
+Command line options
+--------------------
+
+Here are some useful commands for users that do not want to use Emacs,
+or prefer command line tools.
+
+- `-T` do not type check imported .olean files
+
+  % bin/lean -T examples/ex.lean
+
+The option can save you a significant amount of time if you are importing
+many files. Lean still checks the check-sum of the imported files.
+So, it still can detect trivial tempering of the .olean files.
+
+- `-c [file.clean]` create/use a cache file. This option can increase the
+compilation time of large files when we are invoking Lean many times
+with small incremental changes.
+
+  % bin/lean -c ex.clean examples/ex.lean
+
+- `--deps` display files imported by a given Lean file. This option
+is useful if you want to build your own custom Makefile.
+
+  % bin/lean --deps examples/ex.lean
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3437923de..65dc9d4eb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -415,3 +415,6 @@ install(DIRECTORY ${CMAKE_SOURCE_DIR}/../hott DESTINATION ${LIBRARY_DIR}
         PATTERN "*.olean"
         PATTERN ".project"
         PATTERN "TAGS")
+
+install(FILES ${CMAKE_SOURCE_DIR}/../doc/bin/README.md
+        DESTINATION .)