New library material from the AFP entry ZFC_in_HOL

tuned order between theories

bit shifts as class operations

new lemma

don't build Linear_Programming on Mac

tuned comments;

merged

retain type information from reconstruct_proof, notably for Export_Theory.

clarified modules;

tuned proofs;

more robust;

tuned modules;

tuned proofs -- more stable proof terms without [rule_format];

merged

A slight tidying up of messy proof steps

tuned declarations for more compact proof terms;

prefer named facts;

clarified contexts;

tuned messages;

clarified command-line;

tuned messages;

tuned messages;

more messages -- expose potential database problems;

clarified errors: include stdout;

clarified directory;

tuned;

tuned message;

clarified permissions;

merged

discontinued somewhat pointless Isabelle options: setup implicitly assumes…

unused;

support for Phabricator mail configuration;

merged

corrected typo in lemma name

moved lemma

merged

characterization of until in terms of strong until (and vice versa)…

tuned toc

updated to fdb6c5034c24

merged