rearranged setup of arithmetic procedures, avoiding global reference values;

lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);

do nat pass theory value, but sg_ref;

avoid referencing thy value; rename_numerals: use implicit theory context; eliminated some simpset_of Int.thy (why needed anyway?);

avoid referencing thy value; rename_numerals: use implicit theory context;

tuned deps;

tuned;

changed deps;

rename_numerals: use implicit theory context;

avoid referencing thy value; lemma_prat_add_mult_mono moved to PRat.ML;

avoid referencing thy value; lemma_prat_add_mult_mono moved here;

avoid referencing thy value; rename_numerals: use implicit theory context; avoid some simpset_of Int.thy (why needed anyway?);

simpset_of NatDef.thy (why anyway?);

avoid referencing thy value; rename_numerals: use implicit theory context;

avoid referencing thy value;

tuned comment;

avoid global references;

do not pass theory values, but sg_ref;

Drule.merge_rules;

get_names: topologically sorted;

removed all_sessions.graph; improved graph 'directories'; tuned;

removed all_sessions;

disallow duplicates in session identifiers;

assimilated;

tuned HeapFun;

tuned ThmHeap;

removed selector syntax -- improper tuples are broken beyond repair :-(

elim?;

classical atts now intro! / intro / intro?;

renamed "Directories" to "Sessions";