diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 3ec343a0eb..83047789ea 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -21,7 +21,7 @@ namespace tactic -- a term of type 'tactic' into a tactic that sythesizes a term definition and_then (t1 t2 : tactic) : tactic := builtin definition or_else (t1 t2 : tactic) : tactic := builtin -definition append (t1 t2 : tactic) : tactic := builtin +definition par (t1 t2 : tactic) : tactic := builtin definition fixpoint (f : tactic → tactic) : tactic := builtin definition repeat (t : tactic) : tactic := builtin definition at_most (t : tactic) (k : num) : tactic := builtin