#102 (Mar 22, 2016, 7:53:53 AM)

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

Started by user Administrative User