made SML/NJ happy;

clarified Method.section: explicit declaration with static closure;

tuned signature -- define some elementary operations earlier;

discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;

tuned;

tuned;

tuned;

generic euclidean algorithm (due to Manuel Eberl)

integrated appendix theory into main theory; tuned ML

dropped dead file

fix tactic failure with rel_induct0 minimal example: datatype_new 'a A1 = A1 nat and 'a A2 = A2 'a

added jdk-8u20 (inactive);

proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;

support for declaration within token source;

more uniform data slot;

default command position is only valid for default text chunk (amending dcb758188aa6);

tuned -- more total;

tuned;

support for nested Token.src within Token.T; tuned signature;

tuned signature -- moved type src to Token, without aliases;

merged

clarified modules;

added PARALLEL_ALLGOALS convenience;

just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);