restructured matter on polynomials and normalized fractions

streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat

tuned fact references

clarified library contents

standardized notation

redundant

renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b

added lemmas demanded by FIXMEs

dropped comment after conversation with author: predicate compiler works independently from any code generator setup

unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;

tuned signature -- suppress pointless exports;

tuned;

more standard pretty printing; tuned messages;

tuned;

tuned whitespace; tuned comments;

refactored induction principle generation code, for reuse for nonuniform datatypes

merged

consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;

tuned signature -- more abstract type thm_node;

tuned signature;

tuned;

back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);

simplified options;

more careful derivation_closed / close_derivation;

always close derivation, for significantly improved performance without parallel proofs;

tuned whitespace;

removed of_string_limited;

tuned;

tuned;

tuned;