Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)
Summary
- compactified specification of type class parity
- generalized
- explicit annotation of lemma duplicates
- merged
- clarified proof_body: cover zboxes from zproof;
- pro-forma support for optional zproof: no proper content yet;
- clarified signature: follow Term.could_unify;
- clarified bootstrap --- modules related to proofterm.ML;
- clarified path time heuristic: configurable parameters for larger search space;
- clarified heuristics toString; add generator description to schedule;
- tuned;
- add heuristic for non-scheduled (standard) build behaviour;
- proper unused nodes;
- clarified schedule message;
- proper parallel paths;
- clarified build schedule host: more operations;
- clarified path heuristic;
- clarified graph operations in timing heuristic;
- merged
- added and removed [simp]s
Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)
Summary
- adadpted to [simp] changes in distrib
The file was modified | thys/Polynomials/Power_Products.thy |
The file was modified | thys/Progress_Tracking/Combined.thy |
The file was modified | thys/SenSocialChoice/Arrow.thy |