refined activate_notes: simultaneous transformation before activation;
actually export all_registrations_of;
no_document use_thy "Setup";
use "../settings.ML";
use_thy "Numbers";
use_thy "Pairs";
use_thy "Records";
use_thy "Typedefs";
use_thy "Overloading";
use_thy "Axioms";