future_result: explicitly impose Variable.sorts_of again;

recovered a version of dequeue_towards (cf. bb7b5a5942c7); join_results: work only towards explicit dependencies -- otherwise could produce dynamic cycle (not recorded in queue);

added join_bodies;

scheduler: tuned tracing (status); join_wait: more robust is_finished check;

added group_id; added status;

synchronized: tuned tracing;

tuned;

tuned prf_subst: use structure Same;

merged

Changed fact_Suc_nat back to fact_Suc

merged

merged

merged

commit merge

Repairs regarding new Fact.thy.

merged

merged

Use term antiquotation to refer to constant names in subsection title.

Repaired uses of factorial.

Automated merge with http://isabelle.in.tum.de/repos/isabelle

Moved factorial lemmas from Binomial.thy to Fact.thy and merged.

tuned/modernized Envir.subst_XXX;

tuned/modernized subst: Same.operation; renamed typ_subst_TVars to subst_type; renamed subst_TVars to subst_term_types; renamed subst_vars to subst_term; removed unused subst_Vars (covered by subst_term);

tuned;

tuned/modernized Envir operations;

major cleanup, simplification, modernization;

eq_type: special case for empty environment;

compare types directly -- no need to invoke Type.eq_type with empty environment;

incr_indexes (from Proofterm);

tuned incr_indexes;

tuned incr_tvar_same; export tuned version of incr_indexes_same;

added same;