tuned;

tuned GUI;

proper event;

tuned GUI;

build session within running jEdit;

clarified modules;

monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime

more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code

Caratheodory: cleanup and modernisation

restructure fresh variable generation to make exports more wellformed

more canonical context threading

merged

documentation for "Semantic subtype definitions"; misc tuning and simplification;

moved remaining display.ML to more_thm.ML;

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;