diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean
index c70b15f34e..7efa563eb8 100644
--- a/examples/lean/tactic1.lean
+++ b/examples/lean/tactic1.lean
@@ -4,8 +4,14 @@ This example demonstrates how to specify a proof skeleton that contains
 *)
 
 (**
+-- Import useful macros for creating tactics
+import("tactic.lua")
+
 -- Define a simple tactic using Lua
-auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
+auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
+
+conj_hyp = conj_hyp_tac()
+conj     = conj_tac()
 **)
 
 (*
@@ -35,9 +41,9 @@ Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
           let lemma1     : A      := _,  (* first hole *)
               lemma2     : B      := _   (* second hole *)
           in _. (* third hole *)
-   apply auto. done. (* tactic command sequence for the first hole *)
-   apply auto. done. (* tactic command sequence for the second hole *)
-   apply auto. done. (* tactic command sequence for the third hole *)
+   auto. done. (* tactic command sequence for the first hole *)
+   auto. done. (* tactic command sequence for the second hole *)
+   auto. done. (* tactic command sequence for the third hole *)
 
 (*
 In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
@@ -47,9 +53,9 @@ Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
           let lemma1     : A      := _,  (* first hole *)
               lemma2     : B      := _   (* second hole *)
           in _. (* third hole *)
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the first hole *)
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the second hole *)
-   apply conj_tac. apply assumption_tac. done.      (* tactic command sequence for the third hole *)
+   conj_hyp. exact. done.  (* tactic command sequence for the first hole *)
+   conj_hyp. exact. done.  (* tactic command sequence for the second hole *)
+   conj. exact. done.  (* tactic command sequence for the third hole *)
 
 (*
 We can also mix the two styles (hints and command sequences)
@@ -59,7 +65,5 @@ Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
           let lemma1     : A      := _,  (* first hole *)
               lemma2     : B      := _   (* second hole *)
           in (show B /\ A by auto).
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the first hole *)
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the second hole *)
-
-
+   auto. done.  (* tactic command sequence for the first hole *)
+   auto. done.  (* tactic command sequence for the second hole *)
diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean
index 76e542afb8..d6770310d9 100644
--- a/examples/lean/tactic_in_lua.lean
+++ b/examples/lean/tactic_in_lua.lean
@@ -65,7 +65,7 @@
 **)
 
 Theorem T (a b : Bool) : a => b => a /\ b := _.
-   apply (** THEN(REPEAT(ORELSE(imp_tac, conj_in_lua)), assumption_tac) **)
+   (** Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) **)
    done
 
 (* Show proof created using our script *)
diff --git a/src/extra/tactic.lua b/src/extra/tactic.lua
new file mode 100644
index 0000000000..6e8c9af6e5
--- /dev/null
+++ b/src/extra/tactic.lua
@@ -0,0 +1,18 @@
+-- Define macros for simplifying Tactic creation
+local unary_combinator = function (name, fn) tactic_macro(name, { macro_arg.Tactic }, function (env, t) return fn(t) end) end
+local nary_combinator = function (name, fn) tactic_macro(name, { macro_arg.Tactics }, function (env, ts) return fn(unpack(ts)) end) end
+local const_tactic = function (name, fn) tactic_macro(name, {}, function (env) return fn() end) end
+
+unary_combinator("Repeat", Repeat)
+unary_combinator("Try", Try)
+nary_combinator("Then", Then)
+nary_combinator("OrElse", OrElse)
+const_tactic("exact", assumption_tac)
+const_tactic("trivial", trivial_tac)
+const_tactic("absurd", absurd_tac)
+const_tactic("conj_hyp", conj_hyp_tac)
+const_tactic("disj_hyp", disj_hyp_tac)
+const_tactic("unfold_all", unfold_tac)
+const_tactic("beta", beta_tac)
+tactic_macro("apply", { macro_arg.Expr }, function (env, e) return apply_tac(e) end)
+tactic_macro("unfold", { macro_arg.Id }, function (env, id) return unfold_tac(id) end)
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9b53a59fee..154062dec0 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -131,7 +131,7 @@ static unsigned g_level_cup_prec  = 5;
 // are syntax sugar for (Pi (_ : A), B)
 static name g_unused = name::mk_internal_unique_name();
 
-enum class macro_arg_kind { Expr, Exprs, Bindings, Id, String, Comma, Assign, Tactic };
+enum class macro_arg_kind { Expr, Exprs, Bindings, Id, String, Comma, Assign, Tactic, Tactics };
 struct macro {
     list<macro_arg_kind> m_arg_kinds;
     luaref               m_fn;
@@ -140,6 +140,7 @@ struct macro {
 };
 typedef name_map<macro> macros;
 macros & get_expr_macros(lua_State * L);
+macros & get_tactic_macros(lua_State * L);
 macros & get_cmd_macros(lua_State * L);
 
 static char g_set_parser_key;
@@ -207,6 +208,7 @@ class parser::imp {
     frontend_elaborator m_elaborator;
     macros const *      m_expr_macros;
     macros const *      m_cmd_macros;
+    macros const *      m_tactic_macros;
     scanner::token      m_curr;
     bool                m_use_exceptions;
     bool                m_interactive;
@@ -966,6 +968,13 @@ class parser::imp {
         }
     }
 
+    bool is_curr_begin_tactic() const {
+        switch (curr()) {
+        case scanner::token::LeftParen: case scanner::token::Id:    return true;
+        default:                                                    return false;
+        }
+    }
+
     typedef buffer<std::pair<macro_arg_kind, void*>> macro_arg_stack;
     struct macro_result {
         optional<expr>    m_expr;
@@ -1024,6 +1033,14 @@ class parser::imp {
                 tactic t = parse_tactic_expr();
                 args.emplace_back(k, &t);
                 return parse_macro(tail(arg_kinds), fn, prec, args, p);
+            }
+            case macro_arg_kind::Tactics: {
+                buffer<tactic> tactics;
+                while (is_curr_begin_tactic()) {
+                    tactics.push_back(parse_tactic_expr());
+                }
+                args.emplace_back(k, &tactics);
+                return parse_macro(tail(arg_kinds), fn, prec, args, p);
             }}
             lean_unreachable();
         } else {
@@ -1074,6 +1091,17 @@ class parser::imp {
                         case macro_arg_kind::Tactic:
                             push_tactic(L, *static_cast<tactic*>(arg));
                             break;
+                        case macro_arg_kind::Tactics: {
+                            auto const & tactics = *static_cast<buffer<tactic>*>(arg);
+                            lua_newtable(L);
+                            int i = 1;
+                            for (auto t : tactics) {
+                                push_tactic(L, t);
+                                lua_rawseti(L, -2, i);
+                                i = i + 1;
+                            }
+                            break;
+                        }
                         default:
                             lean_unreachable();
                         }
@@ -1461,6 +1489,20 @@ class parser::imp {
         return save(mk_placeholder(), p);
     }
 
+    tactic parse_tactic_macro(name tac_id, pos_info const & p) {
+        lean_assert(m_tactic_macros && m_tactic_macros->find(tac_id) != m_tactic_macros->end());
+        next();
+        auto m = m_tactic_macros->find(tac_id)->second;
+        macro_arg_stack args;
+        flet<bool> set(m_check_identifiers, false);
+        auto r = parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p);
+        if (r.m_tactic) {
+            return *(r.m_tactic);
+        } else {
+            throw parser_error("failed to execute macro, unexpected result type, a tactic was expected", p);
+        }
+    }
+
     /** \brief Parse a tactic expression, it can be
 
         1) A Lua Script Block expression that returns a tactic
@@ -1473,35 +1515,35 @@ class parser::imp {
             parse_script_expr();
             return using_script([&](lua_State * L) {
                     try {
-                        return to_tactic_ext(L, -1);
+                        return to_tactic(L, -1);
                     } catch (...) {
                         throw parser_error("invalid script-block, it must return a tactic", p);
                     }
                 });
+        } else if (curr_is_identifier() && m_tactic_macros && m_tactic_macros->find(curr_name()) != m_tactic_macros->end()) {
+            return parse_tactic_macro(curr_name(), p);
         } else if (curr_is_lparen()) {
             next();
-            flet<bool> set(m_check_identifiers, false);
-            expr pr      = parse_expr();
-            check_rparen_next("invalid apply command, ')' expected");
-            return ::lean::apply_tactic(pr);
+            tactic r = parse_tactic_expr();
+            check_rparen_next("invalid tactic, ')' expected");
+            return r;
         } else {
-           name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
-           optional<object> o = m_env->find_object(n);
-            if (o && (o->is_theorem() || o->is_axiom())) {
-                return ::lean::apply_tactic(n);
-            } else {
-                return using_script([&](lua_State * L) {
-                        lua_getglobal(L, n.to_string().c_str());
-                        try {
-                            tactic t = to_tactic_ext(L, -1);
+            name n = check_identifier_next("invalid tactic, identifier, tactic macro, '(', or 'script-block' expected");
+            return using_script([&](lua_State * L) {
+                    lua_getglobal(L, n.to_string().c_str());
+                    try {
+                        if (is_tactic(L, -1)) {
+                            tactic t = to_tactic(L, -1);
                             lua_pop(L, 1);
                             return t;
-                        } catch (...) {
-                            lua_pop(L, 1);
-                            throw parser_error(sstream() << "unknown tactic '" << n << "'", p);
+                        } else {
+                            throw parser_error(sstream() << "invalid tactic, '" << n << "' is not a tactic in script environment", p);
                         }
-                    });
-            }
+                    } catch (...) {
+                        lua_pop(L, 1);
+                        throw parser_error(sstream() << "unknown tactic '" << n << "'", p);
+                    }
+                });
         }
     }
 
@@ -1734,34 +1776,21 @@ class parser::imp {
     }
 
     /**
-       \brief Execute the <tt>apply [tactic]</tt> tactic command.
+       \brief Execute the tactic.
        This command just applies the tactic to the input state \c s.
        If it succeeds, \c s is assigned to the head of the output
        state sequence produced by the tactic.  The rest/tail of the
        output state sequence is stored on the top of the stack \c
        stack.
     */
-    void apply_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
+    void tactic_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
         auto tac_pos = pos();
-        next();
         tactic t = parse_tactic_expr();
         auto r = apply_tactic(s, t, tac_pos);
         s = r.first;
         stack.push_back(r.second);
     }
 
-    /**
-       \brief Execute the \c assumption tactic command. This command
-       is just syntax sugar for <tt>apply assumption_tac</tt>.
-    */
-    void assumption_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
-        auto tac_pos = pos();
-        next();
-        auto r = apply_tactic(s, assumption_tactic(), tac_pos);
-        s = r.first;
-        stack.push_back(r.second);
-    }
-
     /**
        \brief Execute the \c done tactic command. It succeeds if
        a proof for \c s can be built.
@@ -1799,9 +1828,7 @@ class parser::imp {
                         break;
                     case scanner::token::Id:
                         id = curr_name();
-                        if (id == g_apply) {
-                            apply_cmd(stack, s);
-                        } else if (id == g_back) {
+                        if (id == g_back) {
                             back_cmd(stack, s);
                         } else if (id == g_done) {
                             pr = done_cmd(s, ctx, expected_type);
@@ -1810,13 +1837,13 @@ class parser::imp {
                         } else if (id == g_abort) {
                             next();
                             st = status::Abort;
-                        } else if (id == g_assumption) {
-                            assumption_cmd(stack, s);
                         } else {
-                            next();
-                            throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
+                            tactic_cmd(stack, s);
                         }
                         break;
+                    case scanner::token::ScriptBlock:
+                        tactic_cmd(stack, s);
+                        break;
                     case scanner::token::CommandId:
                         st = status::Abort;
                         break;
@@ -2552,15 +2579,17 @@ public:
         m_scanner.set_command_keywords(g_command_keywords);
         if (m_script_state) {
             m_script_state->apply([&](lua_State * L) {
-                    m_expr_macros = &get_expr_macros(L);
-                    m_cmd_macros  = &get_cmd_macros(L);
+                    m_expr_macros   = &get_expr_macros(L);
+                    m_tactic_macros = &get_tactic_macros(L);
+                    m_cmd_macros    = &get_cmd_macros(L);
                     for (auto const & p : *m_cmd_macros) {
                         m_scanner.add_command_keyword(p.first);
                     }
                 });
         } else {
-            m_expr_macros = nullptr;
-            m_cmd_macros  = nullptr;
+            m_expr_macros   = nullptr;
+            m_tactic_macros = nullptr;
+            m_cmd_macros    = nullptr;
         }
         scan();
     }
@@ -2753,6 +2782,7 @@ expr parse_expr(environment const & env, io_state & ios, std::istream & in, scri
 }
 
 static char g_parser_expr_macros_key;
+static char g_parser_tactic_macros_key;
 static char g_parser_cmd_macros_key;
 DECL_UDATA(macros)
 
@@ -2773,13 +2803,9 @@ macros & get_macros(lua_State * L, char * key) {
     return r;
 }
 
-macros & get_expr_macros(lua_State * L) {
-    return get_macros(L, &g_parser_expr_macros_key);
-}
-
-macros & get_cmd_macros(lua_State * L) {
-    return get_macros(L, &g_parser_cmd_macros_key);
-}
+macros & get_expr_macros(lua_State * L)   { return get_macros(L, &g_parser_expr_macros_key); }
+macros & get_tactic_macros(lua_State * L) { return get_macros(L, &g_parser_tactic_macros_key); }
+macros & get_cmd_macros(lua_State * L)    { return get_macros(L, &g_parser_cmd_macros_key); }
 
 void mk_macro(lua_State * L, macros & mtable) {
     int nargs = lua_gettop(L);
@@ -2816,6 +2842,11 @@ int mk_cmd_macro(lua_State * L) {
     return 0;
 }
 
+int mk_tactic_macro(lua_State * L) {
+    mk_macro(L, get_tactic_macros(L));
+    return 0;
+}
+
 static const struct luaL_Reg macros_m[] = {
     {"__gc",            macros_gc}, // never throws
     {0, 0}
@@ -2829,6 +2860,7 @@ void open_macros(lua_State * L) {
     SET_GLOBAL_FUN(macros_pred, "is_macros");
     SET_GLOBAL_FUN(mk_macro, "macro");
     SET_GLOBAL_FUN(mk_cmd_macro, "cmd_macro");
+    SET_GLOBAL_FUN(mk_tactic_macro, "tactic_macro");
 
     lua_newtable(L);
     SET_ENUM("Expr",     macro_arg_kind::Expr);
@@ -2839,6 +2871,7 @@ void open_macros(lua_State * L) {
     SET_ENUM("Comma",    macro_arg_kind::Comma);
     SET_ENUM("Assign",   macro_arg_kind::Assign);
     SET_ENUM("Tactic",   macro_arg_kind::Tactic);
+    SET_ENUM("Tactics",  macro_arg_kind::Tactics);
     lua_setglobal(L, "macro_arg");
 }
 }
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 211a0851cb..28efa24c51 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -545,35 +545,6 @@ DECL_UDATA(tactic)
     throw exception(sstream() << "arg #" << i << " must be a tactic or a function that returns a tactic");
 }
 
-/**
-   \brief We allow functions (that return tactics) to be used where a tactic
-   is expected. The idea is to be able to write
-          ORELSE(assumption_tactic, conj_tactic)
-   instead of
-          ORELSE(assumption_tactic(), conj_tactic())
-*/
-tactic to_tactic_ext(lua_State * L, int i) {
-    if (is_tactic(L, i)) {
-        return to_tactic(L, i);
-    } else if (lua_isfunction(L, i)) {
-        try {
-            lua_pushvalue(L, i);
-            pcall(L, 0, 1, 0);
-        } catch (...) {
-            throw_tactic_expected(i);
-        }
-        if (is_tactic(L, -1)) {
-            tactic t = to_tactic(L, -1);
-            lua_pop(L, 1);
-            return t;
-        } else {
-            throw_tactic_expected(i);
-        }
-    } else {
-        throw_tactic_expected(i);
-    }
-}
-
 static void check_ios(io_state * ios) {
     if (!ios)
         throw exception("failed to invoke tactic, io_state is not available");
@@ -590,7 +561,7 @@ static int tactic_call_core(lua_State * L, tactic t, ro_environment env, io_stat
 
 static int tactic_call(lua_State * L) {
     int nargs = lua_gettop(L);
-    tactic t = to_tactic_ext(L, 1);
+    tactic t = to_tactic(L, 1);
     ro_shared_environment env(L, 2);
     if (nargs == 3) {
         io_state * ios = get_io_state(L);
@@ -608,36 +579,36 @@ static int nary_tactic(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs < 2)
         throw exception("tactical expects at least two arguments");
-    tactic r = F(to_tactic_ext(L, 1), to_tactic_ext(L, 2));
+    tactic r = F(to_tactic(L, 1), to_tactic(L, 2));
     for (int i = 3; i <= nargs; i++)
-        r = F(r, to_tactic_ext(L, i));
+        r = F(r, to_tactic(L, i));
     return push_tactic(L, r);
 }
 
-static int tactic_then(lua_State * L)           {  return push_tactic(L, then(to_tactic_ext(L, 1), to_tactic_ext(L, 2)));   }
-static int tactic_orelse(lua_State * L)         {  return push_tactic(L, orelse(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
-static int tactic_append(lua_State * L)         {  return push_tactic(L, append(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
-static int tactic_interleave(lua_State * L)     {  return push_tactic(L, interleave(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
-static int tactic_par(lua_State * L)            {  return push_tactic(L, par(to_tactic_ext(L, 1), to_tactic_ext(L, 2))); }
+static int tactic_then(lua_State * L)           {  return push_tactic(L, then(to_tactic(L, 1), to_tactic(L, 2)));   }
+static int tactic_orelse(lua_State * L)         {  return push_tactic(L, orelse(to_tactic(L, 1), to_tactic(L, 2))); }
+static int tactic_append(lua_State * L)         {  return push_tactic(L, append(to_tactic(L, 1), to_tactic(L, 2))); }
+static int tactic_interleave(lua_State * L)     {  return push_tactic(L, interleave(to_tactic(L, 1), to_tactic(L, 2))); }
+static int tactic_par(lua_State * L)            {  return push_tactic(L, par(to_tactic(L, 1), to_tactic(L, 2))); }
 
-static int tactic_repeat(lua_State * L)         {  return push_tactic(L, repeat(to_tactic_ext(L, 1))); }
-static int tactic_repeat1(lua_State * L)        {  return push_tactic(L, repeat1(to_tactic_ext(L, 1))); }
-static int tactic_repeat_at_most(lua_State * L) {  return push_tactic(L, repeat_at_most(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
-static int tactic_take(lua_State * L)           {  return push_tactic(L, take(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
-static int tactic_determ(lua_State * L)         {  return push_tactic(L, determ(to_tactic_ext(L, 1))); }
-static int tactic_suppress_trace(lua_State * L) {  return push_tactic(L, suppress_trace(to_tactic_ext(L, 1))); }
-static int tactic_try_for(lua_State * L)        {  return push_tactic(L, try_for(to_tactic_ext(L, 1), luaL_checkinteger(L, 2))); }
-static int tactic_using_params(lua_State * L)   {  return push_tactic(L, using_params(to_tactic_ext(L, 1), to_options(L, 2))); }
-static int tactic_try(lua_State * L)            {  return push_tactic(L, orelse(to_tactic_ext(L, 1), id_tactic())); }
+static int tactic_repeat(lua_State * L)         {  return push_tactic(L, repeat(to_tactic(L, 1))); }
+static int tactic_repeat1(lua_State * L)        {  return push_tactic(L, repeat1(to_tactic(L, 1))); }
+static int tactic_repeat_at_most(lua_State * L) {  return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
+static int tactic_take(lua_State * L)           {  return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
+static int tactic_determ(lua_State * L)         {  return push_tactic(L, determ(to_tactic(L, 1))); }
+static int tactic_suppress_trace(lua_State * L) {  return push_tactic(L, suppress_trace(to_tactic(L, 1))); }
+static int tactic_try_for(lua_State * L)        {  return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
+static int tactic_using_params(lua_State * L)   {  return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); }
+static int tactic_try(lua_State * L)            {  return push_tactic(L, orelse(to_tactic(L, 1), id_tactic())); }
 
 static int tactic_focus(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 1)
-        return push_tactic(L, focus(to_tactic_ext(L, 1)));
+        return push_tactic(L, focus(to_tactic(L, 1)));
     else if (lua_isnumber(L, 2))
-        return push_tactic(L, focus(to_tactic_ext(L, 1), lua_tointeger(L, 2)));
+        return push_tactic(L, focus(to_tactic(L, 1), lua_tointeger(L, 2)));
     else
-        return push_tactic(L, focus(to_tactic_ext(L, 1), to_name_ext(L, 2)));
+        return push_tactic(L, focus(to_tactic(L, 1), to_name_ext(L, 2)));
 }
 
 static int push_solve_result(lua_State * L, solve_result const & r) {
@@ -677,7 +648,7 @@ static int tactic_solve_core(lua_State * L, tactic t, ro_environment env, io_sta
 
 static int tactic_solve(lua_State * L) {
     int nargs = lua_gettop(L);
-    tactic t = to_tactic_ext(L, 1);
+    tactic t = to_tactic(L, 1);
     ro_shared_environment env(L, 2);
     if (nargs == 3) {
         io_state * ios = get_io_state(L);
@@ -767,11 +738,11 @@ static int mk_lua_cond_tactic(lua_State * L, tactic t1, tactic t2) {
 }
 
 static int mk_lua_cond_tactic(lua_State * L) {
-    return mk_lua_cond_tactic(L, to_tactic_ext(L, 2), to_tactic_ext(L, 3));
+    return mk_lua_cond_tactic(L, to_tactic(L, 2), to_tactic(L, 3));
 }
 
 static int mk_lua_when_tactic(lua_State * L) {
-    return mk_lua_cond_tactic(L, to_tactic_ext(L, 2), id_tactic());
+    return mk_lua_cond_tactic(L, to_tactic(L, 2), id_tactic());
 }
 
 static int mk_id_tactic(lua_State * L)          {  return push_tactic(L, id_tactic()); }
@@ -856,22 +827,22 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_lua_tactic01,       "tactic");
 
     // HOL-like tactic names
-    SET_GLOBAL_FUN(nary_tactic<then>,       "THEN");
-    SET_GLOBAL_FUN(nary_tactic<orelse>,     "ORELSE");
-    SET_GLOBAL_FUN(nary_tactic<interleave>, "INTERLEAVE");
-    SET_GLOBAL_FUN(nary_tactic<append>,     "APPEND");
-    SET_GLOBAL_FUN(nary_tactic<par>,        "PAR");
-    SET_GLOBAL_FUN(tactic_repeat,           "REPEAT");
-    SET_GLOBAL_FUN(tactic_repeat_at_most,   "REPEAT_AT_MOST");
-    SET_GLOBAL_FUN(tactic_repeat1,          "REPEAT1");
-    SET_GLOBAL_FUN(mk_lua_cond_tactic,      "COND");
-    SET_GLOBAL_FUN(mk_lua_when_tactic,      "WHEN");
-    SET_GLOBAL_FUN(tactic_try,              "TRY");
-    SET_GLOBAL_FUN(tactic_try_for,          "TRY_FOR");
-    SET_GLOBAL_FUN(tactic_take,             "TAKE");
-    SET_GLOBAL_FUN(tactic_using_params,     "USING");
-    SET_GLOBAL_FUN(tactic_using_params,     "USING_PARAMS");
-    SET_GLOBAL_FUN(tactic_determ,           "DETERM");
-    SET_GLOBAL_FUN(tactic_focus,            "FOCUS");
+    SET_GLOBAL_FUN(nary_tactic<then>,       "Then");
+    SET_GLOBAL_FUN(nary_tactic<orelse>,     "OrElse");
+    SET_GLOBAL_FUN(nary_tactic<interleave>, "Interleave");
+    SET_GLOBAL_FUN(nary_tactic<append>,     "Append");
+    SET_GLOBAL_FUN(nary_tactic<par>,        "Par");
+    SET_GLOBAL_FUN(tactic_repeat,           "Repeat");
+    SET_GLOBAL_FUN(tactic_repeat_at_most,   "RepeatAtMost");
+    SET_GLOBAL_FUN(tactic_repeat1,          "Repeat1");
+    SET_GLOBAL_FUN(mk_lua_cond_tactic,      "Cond");
+    SET_GLOBAL_FUN(mk_lua_when_tactic,      "When");
+    SET_GLOBAL_FUN(tactic_try,              "Try");
+    SET_GLOBAL_FUN(tactic_try_for,          "TryFor");
+    SET_GLOBAL_FUN(tactic_take,             "Take");
+    SET_GLOBAL_FUN(tactic_using_params,     "Using");
+    SET_GLOBAL_FUN(tactic_using_params,     "UsingParams");
+    SET_GLOBAL_FUN(tactic_determ,           "Determ");
+    SET_GLOBAL_FUN(tactic_focus,            "Focus");
 }
 }
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 5a2acfe952..34ce89e38d 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -312,6 +312,5 @@ tactic normalize_tactic(bool unfold_opaque = false, bool all = true);
 
 UDATA_DEFS_CORE(proof_state_seq)
 UDATA_DEFS(tactic);
-tactic to_tactic_ext(lua_State * L, int i);
 void open_tactic(lua_State * L);
 }
diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean
index 4473dd2730..b1a1c8af5c 100644
--- a/tests/lean/apply_tac1.lean
+++ b/tests/lean/apply_tac1.lean
@@ -1,18 +1,24 @@
+(** import("tactic.lua") **)
+
 Variable f : Int -> Int -> Bool
 Variable P : Int -> Int -> Bool
 Axiom Ax1 (x y : Int) (H : P x y) : (f x y)
 Theorem T1 (a : Int) : (P a a) => (f a a).
-      apply (** imp_tac **)
-      apply (Ax1)
-      assumption
-      done
+      apply Discharge.
+      apply Ax1.
+      exact.
+      done.
 Variable b : Int
 Axiom Ax2 (x : Int) : (f x b)
 (**
-simple_tac = REPEAT(ORELSE(imp_tac, assumption_tac, apply_tac("Ax2"), apply_tac("Ax1")))
+simple_tac = Repeat(OrElse(imp_tac(), assumption_tac(), apply_tac("Ax2"), apply_tac("Ax1")))
 **)
 Theorem T2 (a : Int) : (P a a) => (f a a).
-     apply simple_tac
-     done
+     simple_tac.
+     done.
 
-Show Environment 1.
\ No newline at end of file
+Theorem T3 (a : Int) : (P a a) => (f a a).
+     Repeat (OrElse (apply Discharge) exact (apply Ax2) (apply Ax1)).
+     done.
+
+Show Environment 2.
\ No newline at end of file
diff --git a/tests/lean/apply_tac1.lean.expected.out b/tests/lean/apply_tac1.lean.expected.out
index e8c4c205d8..0d8b2861be 100644
--- a/tests/lean/apply_tac1.lean.expected.out
+++ b/tests/lean/apply_tac1.lean.expected.out
@@ -7,4 +7,6 @@
   Assumed: b
   Assumed: Ax2
   Proved: T2
+  Proved: T3
 Theorem T2 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H)
+Theorem T3 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H)
diff --git a/tests/lean/apply_tac2.lean b/tests/lean/apply_tac2.lean
index 8783499129..1d4beb1167 100644
--- a/tests/lean/apply_tac2.lean
+++ b/tests/lean/apply_tac2.lean
@@ -1,7 +1,8 @@
+(** import("tactic.lua") **)
 Check @Discharge
 Theorem T (a b : Bool) : a => b => b => a.
    apply Discharge.
    apply Discharge.
    apply Discharge.
-   assumption.
+   exact.
    done.
\ No newline at end of file
diff --git a/tests/lean/discharge.lean b/tests/lean/discharge.lean
index 8783499129..1d4beb1167 100644
--- a/tests/lean/discharge.lean
+++ b/tests/lean/discharge.lean
@@ -1,7 +1,8 @@
+(** import("tactic.lua") **)
 Check @Discharge
 Theorem T (a b : Bool) : a => b => b => a.
    apply Discharge.
    apply Discharge.
    apply Discharge.
-   assumption.
+   exact.
    done.
\ No newline at end of file
diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean
index 8b6f55a8a8..d9edf53cd2 100644
--- a/tests/lean/disj1.lean
+++ b/tests/lean/disj1.lean
@@ -1,19 +1,21 @@
+(** import("tactic.lua") **)
+
 Theorem T1 (a b : Bool) : a \/ b => b \/ a.
-    apply imp_tac
-    apply disj_hyp_tac
-    apply disj_tac
+    apply Discharge.
+    (** disj_hyp_tac() **)
+    (** disj_tac() **)
     back
-    apply assumption_tac
-    apply disj_tac
-    apply assumption_tac
-    done
+    exact.
+    (** disj_tac() **)
+    exact.
+    done.
 
 (**
-simple_tac = REPEAT(ORELSE(imp_tac, assumption_tac, disj_hyp_tac, disj_tac)) .. now_tac
+simple_tac = Repeat(OrElse(imp_tac(), assumption_tac(), disj_hyp_tac(), disj_tac())) .. now_tac()
 **)
 
 Theorem T2 (a b : Bool) : a \/ b => b \/ a.
-    apply simple_tac
-    done
+    simple_tac.
+    done.
 
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/disjcases.lean b/tests/lean/disjcases.lean
index a7a3084aa3..ece48f251f 100644
--- a/tests/lean/disjcases.lean
+++ b/tests/lean/disjcases.lean
@@ -1,10 +1,11 @@
+(** import("tactic.lua") **)
 Variables a b c : Bool
 Axiom H : a \/ b
 Theorem T (a b : Bool) : a \/ b => b \/ a.
    apply Discharge.
    apply (DisjCases H).
    apply Disj2.
-   assumption.
+   exact.
    apply Disj1.
-   assumption.
+   exact.
    done.
\ No newline at end of file
diff --git a/tests/lean/interactive/t1.lean b/tests/lean/interactive/t1.lean
index 0934f8f2ec..006c81e412 100644
--- a/tests/lean/interactive/t1.lean
+++ b/tests/lean/interactive/t1.lean
@@ -1,12 +1,12 @@
 Theorem T2 (a b : Bool) : a => b => a /\ b.
 done.
 done.
-apply imp_tac.
-apply imp_tac2.
+(** imp_tac() **).
+imp_tac2.
 foo.
-apply imp_tac.
-apply imp_tac.
-apply conj_tac.
+(** imp_tac() **).
+(** imp_tac() **).
+(** conj_tac() **).
 back.
-apply assumption_tac.
+(** assumption_tac() **).
 done.
diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out
index 139da197ac..c83d8bdae4 100644
--- a/tests/lean/interactive/t1.lean.expected.out
+++ b/tests/lean/interactive/t1.lean.expected.out
@@ -10,10 +10,8 @@ Proof state:
 a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
 ## Proof state:
 H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 8, pos: 6) unknown tactic 'imp_tac2'
-## Error (line: 9, pos: 0) invalid tactic command 'foo'
-Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Error (line: 8, pos: 0) unknown tactic 'imp_tac2'
+## Error (line: 9, pos: 0) unknown tactic 'foo'
 ## Proof state:
 H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
 ## Error (line: 11, pos: 0) tactic failed
diff --git a/tests/lean/interactive/t10.lean b/tests/lean/interactive/t10.lean
index d812556138..5903e27aa5 100644
--- a/tests/lean/interactive/t10.lean
+++ b/tests/lean/interactive/t10.lean
@@ -1,5 +1,5 @@
 (**
-simple_tac = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
+simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
 **)
 
 Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
@@ -8,8 +8,8 @@ Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
                      H2 : B := _,
                      main : B /\ A := _
                  in main).
-   apply simple_tac. done.
-   apply simple2_tac. done.
-   apply simple_tac. done.
+   simple_tac. done.
+   simple2_tac. done.
+   simple_tac. done.
 
 Echo "echo command after failure"
\ No newline at end of file
diff --git a/tests/lean/interactive/t10.lean.expected.out b/tests/lean/interactive/t10.lean.expected.out
index 06ad68cb00..9be33bea02 100644
--- a/tests/lean/interactive/t10.lean.expected.out
+++ b/tests/lean/interactive/t10.lean.expected.out
@@ -6,8 +6,8 @@ A : Bool, B : Bool, H : A ∧ B ⊢ A
 no goals
 ## Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
-## Error (line: 15, pos: 9) unknown tactic 'simple2_tac'
-## Error (line: 15, pos: 22) invalid 'done' command, proof cannot be produced from this state
+## Error (line: 15, pos: 3) unknown tactic 'simple2_tac'
+## Error (line: 15, pos: 16) invalid 'done' command, proof cannot be produced from this state
 Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
 ## Proof state:
diff --git a/tests/lean/interactive/t11.lean b/tests/lean/interactive/t11.lean
index 1621249f20..bac07a73ef 100644
--- a/tests/lean/interactive/t11.lean
+++ b/tests/lean/interactive/t11.lean
@@ -1,5 +1,5 @@
 (**
-auto = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
+auto = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
 **)
 
 Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
@@ -8,7 +8,6 @@ Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
               lemma2     : B      := _,
               conclusion : B /\ A := _
           in conclusion.
-   apply auto. done.
-   apply auto. done.
-   apply auto. done.
-
+   auto. done.
+   auto. done.
+   auto. done.
diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean
index dcec7e53a6..482df80293 100644
--- a/tests/lean/interactive/t12.lean
+++ b/tests/lean/interactive/t12.lean
@@ -1,6 +1,7 @@
 (**
+import("tactic.lua")
 -- Define a simple tactic using Lua
-auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
+auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
 **)
 
 (*
@@ -30,9 +31,9 @@ Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
           let lemma1     : A      := _,  (* first hole *)
               lemma2     : B      := _   (* second hole *)
           in _. (* third hole *)
-   apply auto. done. (* tactic command sequence for the first hole *)
-   apply auto. done. (* tactic command sequence for the second hole *)
-   apply auto. done. (* tactic command sequence for the third hole *)
+   auto. done. (* tactic command sequence for the first hole *)
+   auto. done. (* tactic command sequence for the second hole *)
+   auto. done. (* tactic command sequence for the third hole *)
 
 (*
 In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
@@ -42,9 +43,9 @@ Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
           let lemma1     : A      := _,  (* first hole *)
               lemma2     : B      := _   (* second hole *)
           in _. (* third hole *)
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the first hole *)
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the second hole *)
-   apply conj_tac. apply assumption_tac. done.      (* tactic command sequence for the third hole *)
+   conj_hyp. exact. done.   (* tactic command sequence for the first hole *)
+   conj_hyp. exact. done.   (* tactic command sequence for the second hole *)
+   apply Conj. exact. done. (* tactic command sequence for the third hole *)
 
 (*
 We can also mix the two styles (hints and command sequences)
@@ -54,7 +55,5 @@ Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
           let lemma1     : A      := _,  (* first hole *)
               lemma2     : B      := _   (* second hole *)
           in (show B /\ A by auto).
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the first hole *)
-   apply conj_hyp_tac. apply assumption_tac. done.  (* tactic command sequence for the second hole *)
-
-
+   conj_hyp. exact. done.  (* tactic command sequence for the first hole *)
+   conj_hyp. exact. done.  (* tactic command sequence for the second hole *)
diff --git a/tests/lean/interactive/t13.lean b/tests/lean/interactive/t13.lean
index d1af3886e4..367715bf4f 100644
--- a/tests/lean/interactive/t13.lean
+++ b/tests/lean/interactive/t13.lean
@@ -1,6 +1,6 @@
 (**
 -- Define a simple tactic using Lua
-auto = REPEAT(ORELSE(assumption_tac, conj_tac, conj_hyp_tac))
+auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
 **)
 
 Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
diff --git a/tests/lean/interactive/t2.lean b/tests/lean/interactive/t2.lean
index 544eb7dd69..6af3291327 100644
--- a/tests/lean/interactive/t2.lean
+++ b/tests/lean/interactive/t2.lean
@@ -1,8 +1,8 @@
 Theorem T2 (a b : Bool) : a => b => a /\ b.
-apply imp_tac.
-apply imp_tac2.
+(** imp_tac() **)
+(** imp_tac2() **)
 foo.
-apply imp_tac.
+(** imp_tac() **)
 abort.
 
 Variables a b : Bool.
diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out
index a2ad66205d..bcde59c4bd 100644
--- a/tests/lean/interactive/t2.lean.expected.out
+++ b/tests/lean/interactive/t2.lean.expected.out
@@ -2,14 +2,7 @@
   Set: pp::unicode
 Proof state:
 a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
-## Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 6, pos: 6) unknown tactic 'imp_tac2'
-## Error (line: 7, pos: 0) invalid tactic command 'foo'
-Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
+## Error (line: 6, pos: 0) executing external script ([string "return  imp_tac2() "]:1), attempt to call global 'imp_tac2' (a nil value)
 ## Error (line: 9, pos: 5) failed to prove theorem, proof has been aborted
 Proof state:
 H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean
index 38152b7d3c..7cec59e2b6 100644
--- a/tests/lean/interactive/t3.lean
+++ b/tests/lean/interactive/t3.lean
@@ -1,9 +1,11 @@
+(** import("tactic.lua") **)
+
 Theorem T2 (a b : Bool) : b => a \/ b.
-apply imp_tac.
-apply disj_tac.
+(** imp_tac() **).
+(** disj_tac() **).
 back.
 back.
-assumption.
+exact.
 done.
 
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out
index fb9c744c77..52d917a1cd 100644
--- a/tests/lean/interactive/t3.lean.expected.out
+++ b/tests/lean/interactive/t3.lean.expected.out
@@ -8,7 +8,7 @@ H : b, a : Bool, b : Bool ⊢ a ∨ b
 H : b, a : Bool, b : Bool ⊢ a
 ## Proof state:
 H : b, a : Bool, b : Bool ⊢ b
-## Error (line: 8, pos: 0) failed to backtrack
+## Error (line: 10, pos: 0) failed to backtrack
 Proof state:
 H : b, a : Bool, b : Bool ⊢ b
 ## Proof state:
diff --git a/tests/lean/interactive/t5.lean b/tests/lean/interactive/t5.lean
index f2b60881cc..bbf9c24e35 100644
--- a/tests/lean/interactive/t5.lean
+++ b/tests/lean/interactive/t5.lean
@@ -1,7 +1,8 @@
+(** import("tactic.lua") **)
 Axiom magic (a : Bool) : a.
 
 Theorem T (a : Bool) : a.
-    apply (** apply_tac("magic") **).
+    apply magic.
     done.
 
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/interactive/t6.lean b/tests/lean/interactive/t6.lean
index 502ab937c2..c90acf0517 100644
--- a/tests/lean/interactive/t6.lean
+++ b/tests/lean/interactive/t6.lean
@@ -1,6 +1,7 @@
+(** import("tactic.lua") **)
 Theorem T1 (a b : Bool) : a => b => a /\ b.
-    apply imp_tac.
-    apply imp_tac.
+    (** imp_tac() **).
+    (** imp_tac() **).
     apply Conj.
-    assumption.
+    exact.
     done.
diff --git a/tests/lean/interactive/t7.lean b/tests/lean/interactive/t7.lean
index 094dbbb4b3..4964d81280 100644
--- a/tests/lean/interactive/t7.lean
+++ b/tests/lean/interactive/t7.lean
@@ -1,9 +1,10 @@
+(** import("tactic.lua") **)
 Variable q : Int -> Int -> Bool.
 Variable p : Int -> Bool.
 Axiom Ax (a b : Int) (H : q a b) : p b.
 Variable a : Int.
 Theorem T (x : Int) : (q a x) => (p x).
-    apply imp_tac.
+    (** imp_tac() **).
     apply (Ax a).
-    assumption.
+    exact.
     done.
diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean
index 00609943b9..0d27fce775 100644
--- a/tests/lean/interactive/t8.lean
+++ b/tests/lean/interactive/t8.lean
@@ -1,6 +1,7 @@
+(** import("tactic.lua") **)
 SetOption tactic::proof_state::goal_names true.
 Theorem T (a : Bool) : a => a /\ a.
-   apply imp_tac.
+   apply Discharge.
    apply Conj.
-   assumption.
+   exact.
    done.
diff --git a/tests/lean/interactive/t8.lean.expected.out b/tests/lean/interactive/t8.lean.expected.out
index a63846fcf5..d6c22e416f 100644
--- a/tests/lean/interactive/t8.lean.expected.out
+++ b/tests/lean/interactive/t8.lean.expected.out
@@ -4,10 +4,10 @@
 # Proof state:
 main: a : Bool ⊢ a ⇒ a ∧ a
 ## Proof state:
-main: H : a, a : Bool ⊢ a ∧ a
+main::1: H : a, a : Bool ⊢ a ∧ a
 ## Proof state:
-main::1: H : a, a : Bool ⊢ a
-main::2: H : a, a : Bool ⊢ a
+main::1::1: H : a, a : Bool ⊢ a
+main::1::2: H : a, a : Bool ⊢ a
 ## Proof state:
 no goals
 ##   Proved: T
diff --git a/tests/lean/interactive/t9.lean b/tests/lean/interactive/t9.lean
index c4f5faa97c..73bc3b6bd3 100644
--- a/tests/lean/interactive/t9.lean
+++ b/tests/lean/interactive/t9.lean
@@ -1,3 +1,4 @@
+(** import("tactic.lua") **)
 Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
      Discharge (fun H : A /\ B,
                    let main : B /\ A :=
@@ -5,18 +6,18 @@ Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
                             H2 : A := _
                         in _)
                    in main).
-  apply conj_hyp_tac.
-  assumption.
+  conj_hyp.
+  exact.
   done.
-  apply conj_hyp_tac.
-  assumption.
+  conj_hyp.
+  exact.
   done.
   apply Conj.
-  assumption.
+  exact.
   done.
 
 (**
-simple_tac = REPEAT(ORELSE(conj_hyp_tac, conj_tac, assumption_tac))
+simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
 **)
 
 Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
@@ -25,6 +26,6 @@ Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
                      H2 : B := _,
                      main : B /\ A := _
                  in main).
-   apply simple_tac. done.
-   apply simple_tac. done.
-   apply simple_tac. done.
+   simple_tac. done.
+   simple_tac. done.
+   simple_tac. done.
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index b796eb8a9e..5c1172bb5a 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -1,10 +1,11 @@
+(** import("tactic.lua") **)
 SetOption pp::implicit true
 SetOption pp::coercion true
 SetOption pp::notation false
 Variable vector (A : Type) (sz : Nat) : Type
 Variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 Variable V1 : vector Int 10
-Definition D := read V1 1 (by trivial_tac)
+Definition D := read V1 1 (by trivial)
 Show Environment 1
 Variable b : Bool
 Definition a := b
diff --git a/tests/lean/pr1.lean b/tests/lean/pr1.lean
index c360e15a56..7699472e6d 100644
--- a/tests/lean/pr1.lean
+++ b/tests/lean/pr1.lean
@@ -1,5 +1,6 @@
+(** import("tactic.lua") **)
 Theorem T (C A B : Bool) : C -> A -> B -> A.
-   assumption.
+   exact.
    done.
 
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/slow/tactic1.lean b/tests/lean/slow/tactic1.lean
index 1c8d463923..8c1a4a45a7 100644
--- a/tests/lean/slow/tactic1.lean
+++ b/tests/lean/slow/tactic1.lean
@@ -4,29 +4,29 @@ Definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (doub
 (**
 
  -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
-local congr_tac = REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac))
+local congr_tac = Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
 
 -- Create an eager tactic that only tries to prove goal after unfolding everything
-eager_tac = THEN(-- unfold homogeneous equality
-                 TRY(unfold_tac("eq")),
+eager_tac = Then(-- unfold homogeneous equality
+                 Try(unfold_tac("eq")),
                  -- keep unfolding defintions above and beta-reducing
-                 REPEAT(unfold_tac .. REPEAT(beta_tac)),
+                 Repeat(unfold_tac() .. Repeat(beta_tac())),
                  congr_tac)
 
 -- The 'lazy' version tries first to prove without unfolding anything
-lazy_tac = ORELSE(THEN(TRY(unfold_tac("eq")), congr_tac, now_tac),
+lazy_tac = OrElse(Then(Try(unfold_tac("eq")), congr_tac, now_tac()),
                   eager_tac)
 
 **)
 
 Theorem T1 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
-        apply eager_tac.
+        eager_tac.
         done.
 
 Theorem T2 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
-        apply lazy_tac.
+        lazy_tac.
         done.
 
 Theorem T3 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = ((double (double (double (double (double (double (double f))))))) b).
-        apply lazy_tac.
+        lazy_tac.
         done.
diff --git a/tests/lean/subst2.lean b/tests/lean/subst2.lean
index 0457bdc51d..c688d42f91 100644
--- a/tests/lean/subst2.lean
+++ b/tests/lean/subst2.lean
@@ -1,10 +1,11 @@
+(** import("tactic.lua") **)
 Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z).
    apply ForallIntro.
-   apply beta_tac.
+   beta.
    apply ForallIntro.
-   apply beta_tac.
+   beta.
    apply ForallIntro.
-   apply beta_tac.
+   beta.
    apply Discharge.
    apply Discharge.
    apply Discharge.
diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean
index 5532004482..e6fc74e163 100644
--- a/tests/lean/tactic1.lean
+++ b/tests/lean/tactic1.lean
@@ -3,7 +3,7 @@ Variables p q r : Bool
 (**
  local env = get_environment()
  local conjecture = parse_lean('p => q => p && q')
- local tac = REPEAT(conj_tac() ^ imp_tac() ^ assumption_tac())
+ local tac = Repeat(conj_tac() ^ imp_tac() ^ assumption_tac())
  local proof = tac:solve(env, context(), conjecture)
  env:add_theorem("T1", conjecture, proof)
 **)
diff --git a/tests/lean/tactic10.lean b/tests/lean/tactic10.lean
index 683eae5db4..546d1ef9b2 100644
--- a/tests/lean/tactic10.lean
+++ b/tests/lean/tactic10.lean
@@ -1,23 +1,24 @@
+(** import("tactic.lua") **)
 Definition f(a : Bool) : Bool := not a.
 Definition g(a b : Bool) : Bool := a \/ b.
 
 Theorem T1 (a b : Bool) : (g a b) => (f b) => a := _.
-     apply unfold_tac
-     apply imp_tac
-     apply imp_tac
-     apply disj_hyp_tac
-     assumption
-     apply absurd_tac
+     unfold_all
+     apply Discharge
+     apply Discharge
+     disj_hyp
+     exact
+     absurd
      done.
 
 (**
-simple_tac   = REPEAT(unfold_tac) .. REPEAT(ORELSE(imp_tac, conj_hyp_tac, assumption_tac, absurd_tac, conj_hyp_tac, disj_hyp_tac))
+simple_tac   = Repeat(unfold_tac()) .. Repeat(OrElse(imp_tac(), conj_hyp_tac(), assumption_tac(), absurd_tac(), conj_hyp_tac(), disj_hyp_tac()))
 **)
 
 Definition h(a b : Bool) : Bool := g a b.
 
 Theorem T2 (a b : Bool) : (h a b) => (f b) => a := _.
-     apply simple_tac
+     simple_tac
      done.
 
 Show Environment 1.
diff --git a/tests/lean/tactic11.lean b/tests/lean/tactic11.lean
index 234f7022d1..5bd937c1db 100644
--- a/tests/lean/tactic11.lean
+++ b/tests/lean/tactic11.lean
@@ -1,6 +1,7 @@
+(** import("tactic.lua") **)
 Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a) := _ .
-   apply beta_tac.
-   apply imp_tac.
-   apply conj_hyp_tac.
-   apply assumption_tac.
+   beta.
+   apply Discharge.
+   conj_hyp.
+   exact.
    done.
diff --git a/tests/lean/tactic12.lean b/tests/lean/tactic12.lean
index 19fd699188..fc1193e067 100644
--- a/tests/lean/tactic12.lean
+++ b/tests/lean/tactic12.lean
@@ -1,13 +1,14 @@
+(** import("tactic.lua") **)
 Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a).
-   apply beta_tac.
-   apply imp_tac.
-   apply conj_hyp_tac.
-   apply assumption_tac.
+   beta.
+   apply Discharge.
+   conj_hyp.
+   exact.
    done.
 
 Variables p q : Bool.
 Theorem T2 : p /\ q => q.
-   apply imp_tac.
-   apply conj_hyp_tac.
-   apply assumption_tac.
+   apply Discharge.
+   conj_hyp.
+   exact.
    done.
\ No newline at end of file
diff --git a/tests/lean/tactic13.lean b/tests/lean/tactic13.lean
index cef22110a8..19383f5dfb 100644
--- a/tests/lean/tactic13.lean
+++ b/tests/lean/tactic13.lean
@@ -1,3 +1,4 @@
+(** import("tactic.lua") **)
 Variable f : Int -> Int -> Int
 
 (**
@@ -6,15 +7,15 @@ congr_tac          = apply_tac("Congr")
 symm_tac           = apply_tac("Symm")
 trans_tac          = apply_tac("Trans")
 unfold_homo_eq_tac = unfold_tac("eq")
-auto = unfold_homo_eq_tac .. REPEAT(ORELSE(refl_tac, congr_tac, assumption_tac, THEN(symm_tac, assumption_tac, now_tac)))
+auto = unfold_homo_eq_tac .. Repeat(OrElse(refl_tac, congr_tac, assumption_tac(), Then(symm_tac, assumption_tac(), now_tac())))
 **)
 
 Theorem T1 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a).
-   apply auto.
+   auto.
    done.
 
 Theorem T2 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)).
-   apply auto.
+   auto.
    done.
 
 Show Environment 2.
\ No newline at end of file
diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean
index 81db87befe..93a91da076 100644
--- a/tests/lean/tactic14.lean
+++ b/tests/lean/tactic14.lean
@@ -1,7 +1,7 @@
 (**
 
 -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
-congr_tac = TRY(unfold_tac("eq")) .. REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac))
+congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
 
 **)
 
diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean
index 659ac51529..0c52f1a2bb 100644
--- a/tests/lean/tactic2.lean
+++ b/tests/lean/tactic2.lean
@@ -1,3 +1,4 @@
+(** import("tactic.lua") **)
 Variables p q r : Bool
 
 Theorem T1 : p => q => p /\ q :=
@@ -7,23 +8,30 @@ Theorem T1 : p => q => p /\ q :=
                 H2 : q := _
             in Conj H1 H2
          )).
-    assumption (* solve first metavar *)
+    exact (* solve first metavar *)
     done
-    apply assumption_tac (* solve second metavar *)
+    exact (* solve second metavar *)
     done
 
 (**
-simple_tac = REPEAT(imp_tac() ^ conj_tac() ^ assumption_tac())
+simple_tac = Repeat(imp_tac() ^ conj_tac() ^ assumption_tac())
 **)
 
 Theorem T2 : p => q => p /\ q /\ p := _.
-    apply simple_tac
+    simple_tac
     done
 
 Show Environment 1
 
 Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
-    apply (** REPEAT(ORELSE(imp_tac, conj_tac, conj_hyp_tac, assumption_tac)) **)
+    (** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
+    done
+
+(* Display proof term generated by previous tac *)
+Show Environment 1
+
+Theorem T4 : p => p /\ q => r => q /\ r /\ p := _.
+    Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact)
     done
 
 (* Display proof term generated by previous tac *)
diff --git a/tests/lean/tactic2.lean.expected.out b/tests/lean/tactic2.lean.expected.out
index ce21a11416..e1b42a8943 100644
--- a/tests/lean/tactic2.lean.expected.out
+++ b/tests/lean/tactic2.lean.expected.out
@@ -11,3 +11,10 @@ Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
     Discharge
         (λ H : p,
            Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))
+  Proved: T4
+Theorem T4 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
+    Discharge
+        (λ H : p,
+           Discharge
+               (λ H::1 : p ∧ q,
+                  Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (let H::1::1 := Conjunct1 H::1 in Conj H::2 H::1::1))))
diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean
index d439aa1243..115dcba5a0 100644
--- a/tests/lean/tactic3.lean
+++ b/tests/lean/tactic3.lean
@@ -1,7 +1,8 @@
+(** import("tactic.lua") **)
 Variables p q r : Bool
 
 Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
-    apply (** REPEAT(ORELSE(imp_tac, conj_tac, conj_hyp_tac, assumption_tac)) **)
+    (** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
     done
 
 (* Display proof term generated by previous tactic *)
diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean
index 28cb960718..6181fcfb11 100644
--- a/tests/lean/tactic4.lean
+++ b/tests/lean/tactic4.lean
@@ -1,9 +1,9 @@
 (**
-simple_tac = REPEAT(ORELSE(imp_tac(), conj_tac())) .. assumption_tac()
+simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
 **)
 
 Theorem T4 (a b : Bool) : a => b => a /\ b := _.
-        apply simple_tac
+        simple_tac
         done
 
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic5.lean b/tests/lean/tactic5.lean
index 09ffc63f97..0141839a3e 100644
--- a/tests/lean/tactic5.lean
+++ b/tests/lean/tactic5.lean
@@ -1,9 +1,9 @@
 (**
-simple_tac = REPEAT(ORELSE(imp_tac, conj_tac)) .. assumption_tac
+simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
 **)
 
 Theorem T4 (a b : Bool) : a => b => a /\ b /\ a := _.
-        apply simple_tac
+        simple_tac
         done
 
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic6.lean b/tests/lean/tactic6.lean
index 44a5a98745..355f586c42 100644
--- a/tests/lean/tactic6.lean
+++ b/tests/lean/tactic6.lean
@@ -1,21 +1,22 @@
+(** import("tactic.lua") **)
 Theorem T (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
-   apply imp_tac
-   apply imp_tac
-   apply conj_hyp_tac
-   apply conj_tac
-   apply (** FOCUS(THEN(show_tac, conj_tac, show_tac, assumption_tac), 2) **)
-   apply assumption_tac
+   apply Discharge
+   apply Discharge
+   conj_hyp
+   apply Conj
+   (** Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) **)
+   exact
    done
 
 Theorem T2 (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
-   apply imp_tac
-   apply imp_tac
-   apply conj_hyp_tac
-   apply conj_tac
-   apply show_tac
-   apply (** FOCUS(THEN(show_tac, conj_tac, FOCUS(assumption_tac, 1)), 2) **)
-   apply show_tac
-   apply (** FOCUS(assumption_tac, 1) **)
-   apply show_tac
-   apply (** FOCUS(assumption_tac, 1) **)
+   apply Discharge
+   apply Discharge
+   conj_hyp
+   apply Conj
+   (** show_tac() **)
+   (** Focus(Then(show_tac(), conj_tac(), Focus(assumption_tac(), 1)), 2) **)
+   (** show_tac() **)
+   (** Focus(assumption_tac(), 1) **)
+   (** show_tac() **)
+   (** Focus(assumption_tac(), 1) **)
    done
\ No newline at end of file
diff --git a/tests/lean/tactic8.lean b/tests/lean/tactic8.lean
index 191d1dbb6b..784c1671d1 100644
--- a/tests/lean/tactic8.lean
+++ b/tests/lean/tactic8.lean
@@ -1,8 +1,9 @@
+(** import("tactic.lua") **)
 Theorem T (a b : Bool) : a \/ b => (not b) => a := _.
-     apply imp_tac
-     apply imp_tac
-     apply disj_hyp_tac
-     apply assumption_tac
-     apply absurd_tac
+     apply Discharge
+     apply Discharge
+     disj_hyp
+     exact
+     absurd
      done
 Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean
index a50e896a93..fd59f1aabc 100644
--- a/tests/lean/tactic9.lean
+++ b/tests/lean/tactic9.lean
@@ -1,11 +1,13 @@
+(** import("tactic.lua") **)
 Definition f(a : Bool) : Bool := not a.
 
 Theorem T (a b : Bool) : a \/ b => (f b) => a := _.
-     apply imp_tac
-     apply imp_tac
-     apply disj_hyp_tac
-     apply (** unfold_tac("f") **)
-     apply assumption_tac
-     apply absurd_tac
+     apply Discharge
+     apply Discharge
+     disj_hyp
+     unfold f
+     exact
+     absurd
      done
+
 Show Environment 1.
\ No newline at end of file