doc-src/TutorialI/settings.ML

modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples

(* $Id$ *)

ThyOutput.indent := 5;