more coherent lookup extraction functions

reorganization of code to support DFG otuput

* Pure: 'advanced' translation functions use Context.generic instead of just theory;

declare defn rules;

all styles now reset to defaults first, i.e. the document may switch styles back and forth; added macro \isachardefaults for \chardef defaults; renamed \isakeywordcharunderscore to \isacharunderscorekeyword; added isabellestyle{default};

export meta_rewrite_rule; tuned;

advanced translations: Context.generic; tuned;

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;