diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp
index b3a764645..9b1cbe40f 100644
--- a/src/library/tactic/boolean.cpp
+++ b/src/library/tactic/boolean.cpp
@@ -171,4 +171,25 @@ tactic conj_hyp_tactic(bool all) {
             }
         });
 }
+
+static int mk_conj_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, conj_tactic(nargs == 0 ? true : lua_toboolean(L, 1)));
+}
+
+static int mk_imp_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, imp_tactic(nargs >= 1 ? to_name_ext(L, 1) : name("H"), nargs == 2 ? lua_toboolean(L, 2) : true));
+}
+
+static int mk_conj_hyp_tactic(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_tactic(L, conj_hyp_tactic(nargs == 0 ? true : lua_toboolean(L, 1)));
+}
+
+void open_boolean(lua_State * L) {
+    SET_GLOBAL_FUN(mk_conj_tactic,     "conj_tactic");
+    SET_GLOBAL_FUN(mk_imp_tactic,      "imp_tactic");
+    SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
+}
 }
diff --git a/src/library/tactic/boolean.h b/src/library/tactic/boolean.h
index 1c3daf366..9bf6e2b06 100644
--- a/src/library/tactic/boolean.h
+++ b/src/library/tactic/boolean.h
@@ -10,4 +10,5 @@ namespace lean {
 tactic conj_tactic(bool all = true);
 tactic conj_hyp_tactic(bool all = true);
 tactic imp_tactic(name const & H_name = name("H"), bool all = true);
+void open_boolean(lua_State * L);
 }
diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h
index 03e084c79..2240314dd 100644
--- a/src/library/tactic/register_module.h
+++ b/src/library/tactic/register_module.h
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/tactic/cex_builder.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
+#include "library/tactic/boolean.h"
 
 namespace lean {
 inline void open_tactic_module(lua_State * L) {
@@ -19,6 +20,7 @@ inline void open_tactic_module(lua_State * L) {
     open_cex_builder(L);
     open_proof_state(L);
     open_tactic(L);
+    open_boolean(L);
 }
 inline void register_tactic_module() {
     script_state::register_module(open_tactic_module);
diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean
new file mode 100644
index 000000000..08dc29997
--- /dev/null
+++ b/tests/lean/tactic1.lean
@@ -0,0 +1,11 @@
+Variables p q r : Bool
+
+(**
+ local env = get_environment()
+ local conjecture = parse_lean('p => q => p && q')
+ local tac = REPEAT(conj_tactic() ^ imp_tactic()) .. assumption_tactic()
+ local proof = tac:solve(env, context(), conjecture)
+ env:add_theorem("T1", conjecture, proof)
+**)
+
+Show Environment 1.
diff --git a/tests/lean/tactic1.lean.expected.out b/tests/lean/tactic1.lean.expected.out
new file mode 100644
index 000000000..3e3baf507
--- /dev/null
+++ b/tests/lean/tactic1.lean.expected.out
@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: p
+  Assumed: q
+  Assumed: r
+Theorem T1 : p ⇒ q ⇒ p ∧ q := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H H::1))