reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
use "../settings.ML";
use_thy "Even";
use_thy "Mutual";
use_thy "Star";
use_thy "AB";
use_thy "Advanced";