doc-src/TutorialI/Documents/ROOT.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

use_thy "Documents";