refactor(library/tactic): move 'tracing' tactics to separate module
refactor(library/tactic): move 'exact' tactic to separate module
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): remove unnecessary files
refactor(frontends/lean): remove dead code
refactor(library/tactic): remove unnecessary hack

It is not needed anymore.
We had to use this hack when we had tactic_macro_definition_cell.