diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 6c15592af..796d2bfb0 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -207,4 +207,25 @@ inline tactic determ(tactic const & t) { return take(t, 1); }
    may be infinite or too big.
 */
 tactic force(tactic const & t);
+/**
+   \brief Return a tactic that applies the predicate \c p to the input state.
+   If \c p returns true, then applies \c t1. Otherwise, applies \c t2.
+*/
+template<typename P>
+tactic cond(P && p, tactic const & t1, tactic const & t2) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            return mk_proof_state_seq([=]() {
+                    if (p(env, io, s)) {
+                        return t1(env, io, s).pull();
+                    } else {
+                        return t2(env, io, s).pull();
+                    }
+                });
+        });
+}
+/**
+   \brief Syntax-sugar for cond(p, t, id_tactic())
+*/
+template<typename P>
+tactic when(P && p, tactic const & t) { return cond(std::forward<P>(p), t, id_tactic()); }
 }
diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp
index 8a456db9f..c250f093a 100644
--- a/src/tests/library/tactic/tactic.cpp
+++ b/src/tests/library/tactic/tactic.cpp
@@ -92,6 +92,16 @@ static void tst1() {
     std::cout << "------------------\n";
     std::cout << "proof 2: " << force(take(repeat_at_most(interleave(id_tactic(), id_tactic()), 100) << trace_tactic("foo") << t,
                                            5)).solve(env, io, ctx, q) << "\n";
+
+    std::cout << "proof 2: " << then(cond([](environment const &, io_state const &, proof_state const &) { return true; },
+                                          trace_tactic("then branch.1") + trace_tactic("then branch.2"),
+                                          trace_tactic("else branch")),
+                                     t).solve(env, io, ctx, q) << "\n";
+
+    std::cout << "proof 2: " << then(when([](environment const &, io_state const &, proof_state const &) { return true; },
+                                          trace_tactic("when branch.1") + trace_tactic("when branch.2")),
+                                     t).solve(env, io, ctx, q) << "\n";
+
     std::cout << "done\n";
 }