@@ -842,7 +842,7 @@ runTac autoSolve ist tac
842 when autoSolve solveAll
842 when autoSolve solveAll
843 runT (Induction nm)
843 runT (Induction nm)
844 = do induction nm
844 = do induction nm
845− -- when autoSolve solveAll
845+ when autoSolve solveAll
846 runT (LetTac n tm)
846 runT (LetTac n tm)
847 = do attack
847 = do attack
848 tyn <- unique_hole (MN 0 "letty")
848 tyn <- unique_hole (MN 0 "letty")