removed conditional combinator;
avoid handle _;
showctxt: print_context (cf. local theory context);
searchtheorems: proper find_theorems;
refrain from setting ml_prompts again;
tuned init_pgip;
use "../settings";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
use_thy "Nested2";