diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 3a2237d9c..ce466fa8d 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -247,4 +247,24 @@ tactic repeat_at_most(tactic t, unsigned k) {
             }
         });
 }
+
+tactic take(tactic t, unsigned k) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            tactic _t(t);
+            return take(k, _t(env, io, s));
+        });
+}
+
+tactic force(tactic t) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            tactic _t(t);
+            proof_state_seq r = _t(env, io, s);
+            buffer<proof_state> buf;
+            for (auto s2 : r) {
+                buf.push_back(s2);
+                check_interrupted();
+            }
+            return to_lazy(to_list(buf.begin(), buf.end()));
+        });
+}
 }
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index df5eb14d5..12288a2f1 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -132,4 +132,22 @@ tactic repeat(tactic t);
    then tactic \c t will be applied 2^k times.
 */
 tactic repeat_at_most(tactic t, unsigned k);
+/**
+   \brief Return a tactic that applies \c t, but takes at most \c
+   k elements from the sequence produced by \c t.
+*/
+tactic take(tactic t, unsigned k);
+/**
+   \brief Return a tactic that forces \c t to produce all
+   the elements in the resultant sequence.
+
+   \remark proof_state_seq is a lazy-list, that is, their
+   elements are produced on demand. This tactic forces
+   all the elements in the sequence to be computed eagerly.
+
+   \remark The sequence may be infinite. So, consider
+   combining this tactical with \c take if the sequence
+   may be infinite or too big.
+*/
+tactic force(tactic t);
 }
diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp
index 444909417..b0757cdfd 100644
--- a/src/tests/library/tactic/tactic.cpp
+++ b/src/tests/library/tactic/tactic.cpp
@@ -89,8 +89,8 @@ static void tst1() {
 
     std::cout << "proof 2: " << orelse(then(repeat_at_most(append(msg_tactic("hello1"), msg_tactic("hello2")), 5), fail_tactic()),
                                        t).solve(env, io, ctx, q) << "\n";
-
-
+    std::cout << "------------------\n";
+    std::cout << "proof 2: " << force(take(then(repeat_at_most(interleave(id_tactic(), id_tactic()), 100), then(msg_tactic("foo"), t)), 5)).solve(env, io, ctx, q) << "\n";
     std::cout << "done\n";
 }