Summary
- document that n2m does not depend on most things in fp_sugar in its type
- clarified rule structure;
- accomodate Isabelle identifiers with subscripts;
- more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
- eliminated unused argument (see also 58110c1e02bc);
- add le_log_of_power and le_log2_of_power by Tobias Nipkow
- unified CHAR with CHR syntax