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 "PDL";
use_thy "CTL";
use_thy "CTLind";