diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean
index 88d40df87..a0d264e13 100644
--- a/library/standard/tactic.lean
+++ b/library/standard/tactic.lean
@@ -27,6 +27,7 @@ definition id         : tactic := tactic_value
 definition beta       : tactic := tactic_value
 definition apply      {B : Type} (b : B) : tactic := tactic_value
 definition unfold     {B : Type} (b : B) : tactic := tactic_value
+definition exact      {B : Type} (b : B) : tactic := tactic_value
 definition trace      (s : string) : tactic := tactic_value
 infixl `;`:200         := and_then
 infixl `|`:100         := or_else
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index cee52e379..f3b3bccff 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -60,18 +60,6 @@ void collect_simple_meta(expr const & e, buffer<expr> & metas) {
         });
 }
 
-/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
-void check_has_no_local(expr const & v, expr const & e) {
-    if (has_local(v)) {
-        for_each(v, [&](expr const & l, unsigned) {
-                if (is_local(l))
-                    throw tactic_exception(e, sstream() << "apply tactic contains reference to local '" << local_pp_name(l)
-                                           << "' which is not marked as [fact], so it is not visible to tactics");
-                return has_local(l);
-            });
-    }
-}
-
 tactic apply_tactic(expr const & _e) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
@@ -100,7 +88,7 @@ tactic apply_tactic(expr const & _e) {
                     type_checker tc(env, new_ngen.mk_child());
                     expr new_e = subst.instantiate(e);
                     expr new_p = g.abstract(new_e);
-                    check_has_no_local(new_p, _e);
+                    check_has_no_local(new_p, _e, "apply");
                     substitution new_subst = subst.assign(g.get_name(), new_p);
                     buffer<expr> metas;
                     collect_simple_meta(new_e, metas);
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index e815f33cb..fce79abd1 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -110,6 +110,9 @@ static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr c
 static register_tac reg_apply(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) {
         return apply_tactic(app_arg(e));
     });
+static register_tac reg_exact(name(g_tac, "exact"), [](type_checker &, expr const & e, pos_info_provider const *) {
+        return exact_tactic(app_arg(e));
+    });
 static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) {
         expr id = get_app_fn(app_arg(e));
         if (!is_constant(id))
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index f01098b9f..51c4290bd 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -13,12 +13,27 @@ Author: Leonardo de Moura
 #include "util/lazy_list_fn.h"
 #include "util/list_fn.h"
 #include "kernel/instantiate.h"
+#include "kernel/type_checker.h"
+#include "kernel/for_each_fn.h"
 #include "kernel/replace_visitor.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/tactic.h"
 #include "library/io_state_stream.h"
 
 namespace lean {
+/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
+void check_has_no_local(expr const & v, expr const & e, char const * tac_name) {
+    if (has_local(v)) {
+        for_each(v, [&](expr const & l, unsigned) {
+                if (is_local(l))
+                    throw tactic_exception(e, sstream() << "tactic '" << tac_name << "' contains reference to local '" << local_pp_name(l)
+                                           << "' which is not visible by this tactic "
+                                           << "possible causes: it was not marked as [fact]; it was destructued");
+                return has_local(l);
+            });
+    }
+}
+
 tactic_exception::tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {}
 tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {}
 
@@ -205,6 +220,26 @@ tactic assumption_tactic() {
         });
 }
 
+tactic exact_tactic(expr const & _e) {
+    return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
+            type_checker tc(env);
+            substitution subst  = s.get_subst();
+            goals const & gs    = s.get_goals();
+            goal const & g      = head(gs);
+            expr e              = subst.instantiate(_e);
+            expr e_t            = subst.instantiate(tc.infer(e));
+            expr t              = subst.instantiate(g.get_type());
+            if (tc.is_def_eq(e_t, t) && !tc.next_cnstr()) {
+                expr new_p = g.abstract(e);
+                check_has_no_local(new_p, _e, "exact");
+                substitution new_subst = subst.assign(g.get_name(), new_p);
+                return some(proof_state(s, tail(gs), new_subst));
+            } else {
+                return none_proof_state();
+            }
+        });
+}
+
 tactic beta_tactic() {
     return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             bool reduced = false;
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 789ac11d2..2fb52a192 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -14,6 +14,9 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 
 namespace lean {
+/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
+void check_has_no_local(expr const & v, expr const & e, char const * tac_name);
+
 class tactic_exception : public exception {
     expr m_expr;
 public:
@@ -132,6 +135,8 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_
 */
 tactic focus(tactic const & t, unsigned i);
 inline tactic focus(tactic const & t) { return focus(t, 1); }
+/** \brief Solve first goal iff it is definitionally equal to \c e */
+tactic exact_tactic(expr const & e);
 /** \brief Return a tactic that unfolds the definition named \c n. */
 tactic unfold_tactic(name const & n);
 /** \brief Return a tactic that unfolds all (non-opaque) definitions. */
diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean
new file mode 100644
index 000000000..37db1fc8b
--- /dev/null
+++ b/tests/lean/run/tactic12.lean
@@ -0,0 +1,16 @@
+import standard
+using tactic
+
+theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
+:= by apply and_intro;
+      apply not_intro;
+      exact
+        (assume Ha, or_elim H
+          (assume Hna, absurd Ha Hna)
+          (assume Hnb, absurd Hb Hnb));
+      assumption
+
+
+
+
+