tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
activate_notes in parallel -- to speedup main operation of locale interpretation;
refined activate_notes: simultaneous transformation before activation;
actually export all_registrations_of;
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
updated polyml/build option to prefer included libffi;