removed Misc/Translations (text covered by Documents.thy);

Redundant patterns no longer cause errors.

Code generator now adds type constraints to val declarations (to make SML/NJ happy).

tuned;

updated;

removed Types/records.tex;

added add_fixes: derives mssing type scheme from mixfix;

fixed inst_thm: proper domain of env; flatten_expr: collective import elements over *all* imports; use ProofContext.add_fixes; disallow term bindings in locale body elements;

tuned;

added lemma;