added translations for SORT_CONSTRAINT tuned;

conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;

added make;

maintain sort occurrences of declared terms;

added weaken_sorts; strip_shyps: minimal list of minimized extra sorts; tuned;

added make, minimal_sorts;

added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;

added check_shyps, which reject pending sort hypotheses;

Drule.norm_hhf_eqs;

prove_common: include all sorts from context into statement, check shyps of result; Drule.norm_hhf_eqs;

added rules for sort_constraint, include in norm_hhf_eqs; tuned;

tuned;

avoid accidental dependency of automated proof on sort equiv;

explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;

avoid CRITICAL with_path;

rewrite more proofs in Isar style

Removed ex/Locales.thy.

More occurrences of 'includes' gone.

Removed outdated locales tutorial.

correct rounding

circumvent some TeX problem

only test HOL image for smlnj

tuned;

tuned;