diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean
index 72ce998b7..81ac7fb8d 100644
--- a/examples/lean/ex4.lean
+++ b/examples/lean/ex4.lean
@@ -2,5 +2,5 @@ Definition a : Nat := 10
 (* Trivial indicates a "proof by evaluation" *)
 Theorem T1 : a > 0 := Trivial
 Theorem T2 : a - 5 > 3 := Trivial
-(* The next one fails *)
-Theorem T3 : a > 11 := Trivial
+(* The next one is commented because it fails *)
+(* Theorem T3 : a > 11 := Trivial *)
diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean
index 71974dc8e..c18daf11d 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 (** REPEAT(ORELSE(imp_tactic, conj_in_lua)) .. assumption_tactic **)
+   apply (** REPEAT(ORELSE(imp_tac, conj_in_lua)) .. assumption_tac **)
    done
 
 (* Show proof created using our script *)
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index aafe5179f..033bba4d7 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -3,11 +3,17 @@ include_directories("${LEAN_BINARY_DIR}")
 add_executable(lean lean.cpp)
 add_dependencies(lean githash)
 target_link_libraries(lean ${EXTRA_LIBS})
-add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
-add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex2.lean")
-add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex3.lean")
+
 add_test(example1_stdin ${CMAKE_CURRENT_BINARY_DIR}/lean < "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
 
+# LEAN EXAMPLES
+file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/lean/*.lean")
+FOREACH(T ${LEANEXAMPLES})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanex_${T_NAME}"
+    COMMAND ${CMAKE_CURRENT_BINARY_DIR}/lean ${T})
+ENDFOREACH(T)
+
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
 FOREACH(T ${LEANTESTS})