less redundant output;

proper context;

tuned;

tuned;

tuned;

tuned signature: eliminated pointless type Context.pretty;

more explicit Defs.context: use proper name spaces as far as possible;

explicit indication of overloaded typedefs;

tuned signature;

tuned output;

tuned output;

tuned signature;

eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;

tuned signature;

tuned output;

separate command 'print_definitions';

tuned;

clarified deps entry: global names for arguments;

renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing;

tuned signature;

tuned whitespace;

HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;

prove Liminf_inverse_ereal

merged

exchange uniform limit and integral

congruence rules for the relator

conceal only the definitional theorems of map, set, rel (and not the actual constants)

more useful properties of the relators

tuned proofs (less warnings)

Useful facts about min/max, etc.