added sumEN_tupled_balanced

load fonts into JavaFX as well;

some support for actual HTML rendering;

merged

free variable name tuning

reuse generated names (they look better + slightly more efficient)

desambiguate grammar (e.g. for Nil's mixfix ("[]"))

avoided duplicate lemma

put an underscore between names, for compatibility with old package (and also because it makes sense)

got rid of metis calls

tuning

removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);

standardized ML aliases;

tuned headers;

avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);

discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);

more robust interrupt handling;

some attempts to synchronize ROOT/files and document/build;

tuned error;

option_pred characterization

true vs. True in pattern matching

reduced theory dependencies

tuning

moved theorems closer to where they are used

tuning

renamed "Ordinals_and_Cardinals" to "Cardinals"

split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF

reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping

tuning

tuning annotations