more ambitious test;

added lemmas and tuned proofs

merged

Switching to inverse image and constant_on, plus some new material

proper integer option for Admin/build_history;

clarified output;

tuned output;

more thorough treatment of afp_version and afp_pull_date;

tuned options;

tuned output;