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;

tuned map_proof_terms_option; eliminated apsome, apsome'; tuned;

export incr_tvar_same; tuned;

added map_option;

use structure Same;

use structure Same; tuned;

use structure Same; do not open Envir;

use structure Same; tuned signature; tuned comments; tuned;

added map;

use structure Same; more exports; tuned;

Support for copy-avoiding functions on pure values, at the cost of readability.

removed obsolete/unused legacy_varify;

eliminated legacy_varify;

merged

simplified proofs

more antiquotations;