diff --git a/doc/bin/README.md b/doc/bin/README.md
index 2e05b02c2c..586389e980 100644
--- a/doc/bin/README.md
+++ b/doc/bin/README.md
@@ -23,28 +23,3 @@ 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
---------------------
-
-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