doc-src/TutorialI/settings.ML

failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is

(* $Id$ *)

ThyOutput.indent := 5;