feat(frontends/lean): remove tactic hints for specific classes

The idea is to separate class-instance resolution and tactic framework
as two independent engines.
refactor(frontends/lean/tactic_hint): simplify tactic_hints
fix(bin/linja): add 'all' to phony target; allow multiple phony targets
fix(shell/lean.cpp): print git commit in version string only when it's available
feat(src): add LEAN_VERSION_PATCH
chore(CMakeLists.txt): standard_lib target generates TAGS for library
fix(CMakeLists.txt): rename EMACS_LIB to EMACS_LISP_DIR (default: share/eamcs/site-lisp/lean)
feat(CMakeLists.txt): install lean library to LIBRARY_DIR (default: lib/lean)
fix(bin): use "python" instead of "python2" or "python2.7"
feat(util/lean_path.cpp): add "exe_path/../lib/lean" to LEAN_PATH

Related issue: #223
fix(emacs): support tabs in a file

Fix #226
fix(bin/ltags): add option --relative to handle path relatively

Fix #230
fix(frontends/lean/elaborator): 'as-is' expressions

The elaborator should not introduce implicit arguments on terms marked
as 'as-is'.
refactor(kernel/macro_definition_cell): improve macro get_type API
feat(CMakeLists.txt): use bin/package_version if needed

1) When git sha1 is available:

    Lean (version 0.2.0, commit 4a119a042435, Release)

2) When git sha1 is not available, but there is bin/package_version file

    Lean (version 0.2.0, package 0.2.0~ubuntu1~12.04, Release)

3) Git sha1 is not available, bin/package_version does not exist.

    Lean (version 0.2.0, Release)

Close #229
refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument
feat(frontends/lean/class): accept only inductive datatypes (and records) as classes
feat(frontends/lean/builtin_cmds): add 'print classes' command
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228
doc(syntax_highlight_in_latex.md): explain how to use minted and Pygments