doc-src/TutorialI/settings.ML

reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers

Thy_Output.indent_default := 5;