PureThy.note_thmss_i;

added exit; notes: simplified locale target;

added theorems(_i) -- with present_results;

def(_i): LocalDefs.add_defs; removed Drule.strip_shyps_warning;

attribute: Context.mapping; removed Drule.strip_shyps_warning;

removed obsolete note_thmss(_i); simplified add_thmss; tuned;

added exit;

simplified derived_def;

removed theorems, smart_theorems etc. (cf. Specification.theorems);

lemmas/theorems/declare: Specification.theorems;

added kind attributes;

Drule.lhs/rhs_of;

added dest_equals_lhs; replaced clhs/crhs_of by lhs/rhs_of; local_standard: flexflex_unique; removed strip_shyps_warning;

attribute: Context.mapping; Proof.theorem_i;

replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;

attribute: Context.mapping; PureThy.note_thmss_i;

standardized facts;

attribute symmetric: zero_var_indexes; tuned proofs;

attribute symmetric: zero_var_indexes;

attribute: Context.mapping;

cleaned up interfaces

Removed unused res_atp_setup.ML, since its functions have been put in res_atp.ML.

Common theory targets.

Element.export_facts;

refined unlocalize_mixfix;

TheoryTarget;

moved pretty_consts to proof_display.ML; adapted to improved LocalTheory interfaces;

added pretty_consts (from specification.ML);

turned into abstract wrapper module, cf. theory_target.ML; simplified interfaces;

replaced add_def by more elaborate add_defs; added find_def (based on educated guesses);