diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index fd283a75eb..8e093ba641 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -136,11 +136,6 @@ by { macro «try» t:tactic : tactic => `($t <|> skip) -syntax "repeat" tactic : tactic -macro_rules -| `(tactic| repeat $t) => `(tactic| try ($t; repeat $t)) - - theorem simple12 (x y z : Nat) : y = z → x = x → x = y → x = z := by { intro h1; intro h2; intro h3;