reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
use_thy "Basic";
use_thy "Blast";
use_thy "Force";
use_thy "Forward";
use_thy "Tacticals";
use_thy "find2";