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

use "../settings.ML";
use_thy "Ifexpr";