From c85d6d5a1eec15b081a62b18d3672c554736bad0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Feb 2016 16:10:35 -0800 Subject: [PATCH] fix(library/init/tactic): typo --- library/init/tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 3ec343a0e..83047789e 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