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";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
use_thy "Nested2";