verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization), custom-made (top-down) atomize_conv, store predicate and function symbols in a table instead of a list for faster lookup, updated certificates

merged

tuned proofs

tuned lattices theory fragements; generlized some lemmas from sets to lattices

avoid lazy val with side-effects -- spurious null pointers!?

toString: more robust handling of null; tuned;

proper markup text for loc;

output_syms: permissive treatment of control symbols, cf. Scala version;

basic treatment of special control symbols; misc tuning;