added map_atype, map_aterms

tuned proof;

declare atomize/defn for Ball;

invent_fixes: merely enter body temporarily;

'unfolding': LocalDefs.unfold;

moved treatment of object-logic equalities to local_defs.ML;

method (un)folded: option '(raw)';

added attributes defn_add/del; added (un)fold operations (from object_logic.ML); tuned;

added 'defn' attribute; attribute (un)folded: option '(raw)';

proper order of trfuns;

CPure: Context.add_setup;

tuned proofs;

implicit setup;

default rule step: norm_hhf_tac;

tuned comment;

declare 'defn' rules;

LocalDefs;

Basic operations on local definitions.

removed unnecessary Syntax.fix_mixfix;

added axiomatization_loc, definition_loc; definition: let LocalDefs.derived_def do the actual work;

moved local defs to local_defs.ML;

LocalDefs; unfolding(_i): support object-level rewrites;

removed unatomize; added versions of meta_rewrite, unfold, fold;

(un)fold: support object-level rewrites;

added print_consts; tuned;

removed obsolete keyword 'files';

(un)folded: support object-level rewrites;

added equals_cong;

added Isar/local_defs.ML;

LocalDefs.add_def;