feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
fix(library/data/prod): make the notation for tuples and product types consistent
fix(emacs/lean-syntax): syntax highlight for declarations with explicit universes
test(tests/lean/run): expand tree example
fix(frontends/lean/decl_cmds): error messages
feat(frontends/lean): add option '-X': discard all proofs after theorems are checked

This option is useful for generating compact .olean files for web demos
feat(library/kernel_serializer): compress binder modifier annotations when saving .olean file
refactor(frontends/lean/parser): add missing 'const'
feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem
chore(version): bump universe level to force .olean recompilation
feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration
refactor(library/algebra/category/morphism): make sure bug #231 has been fixed
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
fix(library/module): allow multiple calls to import_modules with the same modules

The idea is to store a set of already imported files.
This feature is useful when using the import_modules API directly (e.g.,
from javascript).
chore(library/Makefile): remove unused Makefile
feat(emacs/lean-type): add lean-show-type-add-to-kill-ring option

If a customization option 'lean-show-type-add-to-kill-ring' is non-nil
and a user runs 'lean-show-type' by explicitly typing 'C-c C-t',
lean-mode saves the displayed type information message into kill-ring
, which can be pasted by yank (C-y) command.

Close #245
fix(library/module): race condition on m_imported
fix(kernel/constraint): bug in operator<<
feat(kernel/converter): relax is_def_eq test for local constants and meta-variables
chore(library/simplifier): delete old simplifier

This was the simplifier used in Lean 0.1.