advanced translations: Context.generic;

tidy-up of res_clause.ML, removing the "predicates" field

'setup': no list type, support implicit setup; tuned;

'fixes': support plain vars; classical attributes: optional weight -- ignored by automated tools;

fixed a syntax error!

replaced gen_list by enum

adaptions to codegen_package

various improvements

added three times overloaded Isar instance command

moved instance Isar command to class_package.ML

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.