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