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