cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; avoid rep_theory;

removed Pure/Syntax/ROOT.ML;

Term.string_of_vname;

Theory.inferT_axm;

do not enable Toplevel.debug globally;

cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;

canonical merge operations

declarations: apply target_morphism;

inst(T)_morphism: avoid reference to static theory value;

tuned signature; export: precomputed closure, no reference to contexts;

added Morphism.transform/form (generic non-sense);

Morphism.transform/form;

data declaration: removed obsolete target_morphism (still required for local data!?);

data declaration: removed obsolete target_morphism;

added eval_antiquotes_fn (tmp);

tuned document (headers, sections, spacing);

do translation: CONST;

eval_antiquotes: proper parentheses for projection;

canonical merge operations

Removed erroneous application of rev in get_clauses that caused introduction rules taken from the InductivePackage database to be in the wrong order.

more robust proof

Experimental code for the interpretation of definitions.

Experimental interpretation code for definitions.

New file for locale regression tests.

debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal

minimize imports

new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports

moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy

added proj_value_antiq;

absdummy: use internal name uu to avoid renaming of popular names;