From 905a1095f9a7ba7fef1068d2294bd21d5be8a05c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jul 2014 23:41:23 -0700 Subject: [PATCH] fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore Signed-off-by: Leonardo de Moura --- tests/lean/run/tactic14.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean index 304db5703..4a5f67b63 100644 --- a/tests/lean/run/tactic14.lean +++ b/tests/lean/run/tactic14.lean @@ -2,7 +2,7 @@ import standard using tactic definition basic_tac : tactic -:= repeat [apply @and_intro | apply @not_intro | assumption] +:= repeat [apply @and_intro | assumption] set_proof_qed basic_tac -- basic_tac is automatically applied to each element of a proof-qed block