@@ -44,6 +44,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
4444 , ("reflect", Just ExprTArg)
4545 , ("fill", Just ExprTArg)
4646 , ("try", Just AltsTArg)
47+ , ("induction", Just NameTArg)
4748 ] ++ map (\x -> (x, Nothing)) [
4849 "intros", "compute", "trivial", "solve", "attack",
4950 "state", "term", "undo", "qed", "abandon", ":q"