Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs

notes: proper naming of thm proof, activated import_export_proof;

added full_name;

notes: more careful treatment of Goal.close_result; tuned;

note_thmss: refrain from closing the derivation here;

notes: proper import/export of proofs (still inactive); Goal.norm/close_result; tuned;

removed obsolete (export_)standard;

added mixfix';

added merge_list;

zero_var_indexes_inst: multiple terms; tuned;

Theory.merge_list;

qualified MetaSimplifier.norm_hhf(_protect);

added norm/close_result (supercede local_standard etc.);

added zero_var_indexes_list; removed local_standard (cf. Goal.norm/close_result); instantiate: more precise handling of indexes;

Goal.norm/close_result;

simplified syntax for 'definition', 'abbreviation';

*** bad commit -- reverted to previous version ***

removed export_standard_morphism; Assumption.assms_of: cterm;

simplified add_thmss; mark predicate definitions as internal;

added map/burrow_facts; exported name_multi, name_thm;

added INCR_COMP, COMP_INCR;

tuned;

reworked notes: towards proper import/export of proof terms; tuned;

removed export_standard_morphism;

renamed SIMPLE_METHOD' to SIMPLE_METHOD''; added simple version of SIMPLE_METHOD';

added export; removed find_def, expand_defs;

tuned spaces/comments;

simplified method setup; reactivated dead code;

simplified method setup;

simplified method setup; tuned oracle setup;