unfold intermediate definitions after sealing the bnf

bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned

tuned; elimination rule subset_imageE; typical composition collapsing rewrite order in lemma image_image_eq_image_comp; destruction rules ball_imageD, bex_imageD

more careful unfolding of internal constants

made typedef for the type of the bound optional (size-based)

made natLe{q,ss} constants (yields smaller terms in composition)

removed junk

tuned proofs;

unused;

tuned;

more formal read_root;

simplified / modernized hide commands: proper outer parsers and PIDE markup via check;

removed dead code;

check fact names with PIDE markup;

tuned signature;

do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);

tuned proofs;

tuned proofs;

keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context;

modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;

allow suffix of underscores for words (notably keywords), similar to semantic completion;

back to polyml-svn, with more threads to avoid problems with HOL-Proofs (see f376f18fd0b7);

no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;

clarified description; tuned;

tuned;

tuned proofs;

more antiquotations;

ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");