replaced Undef by UU;

converted theory Lift;

rep_datatype lift; converted to new-style theory;

moved into Main;

moved String into Main;

tuned;

HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac instead of lift.induct_tac, use UU instead of Undef in cases;

declare transitive;

theory Calculation move to Set;

transitive declared in Pure;

Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.

Goals.add_locale;

fix_frees; improved export_def: handle args on lhs;

theorem: locale argument;

beginnings of new locales (not yet functional);

Goals.setup;

parking code for old-style locales here;

tuned notation (degree instead of dollar);

theorem(_i): locale argument; contexts 0 and 1 in state now refer to theory and locale, respectively; unified export (no longer uses global "standard");

Proof.init_state thy None;

simplified export; tuned printing of fixes;

'atomize': CHANGED_PROP;

global statements: locale argument;

added local_standard;