doc-src/TutorialI/Ifexpr/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 "../settings.ML";
use_thy "Ifexpr";