make 'typedef' optional, depending on size of original type

use aconv to compare terms (for cleanliness)

tuning

optimize cardinal bounds involving natLeq (omega)

no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');

merged

more standard module name;

silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;

tuned whitespace;

allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;

tuned proofs;

prefer Name_Space.check with its builtin reports (including completion);

tuned source structure;

prefer Name_Space.check with its builtin reports (including completion);

consider completion report as part of error message -- less stateful, may get handled;

more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;

more antiquotations;

clarified names of antiquotations and markup; more documentation;

tuned proof

merged

tuned proofs

repaired document;

repaired document;

more markup for ML source;

merged

tuned signature;

clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";

clarified module structure;

tuned;

tuned signature -- separate module Font_Info;