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);

tuned signature;

more compact datatypes;

tuned;

clarifed Method.evaluate: turn text into semantic method (like Basic);

simplified type Proof.method;

more general dummy: may contain "parked arguments", for example;

document 'ctr_transfer'

generate 'ctr_transfer' for (co)datatypes

rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup

Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)

reduced dependency on 'Datatype' theory and ML module

removed Z3 3.2, now superseded by Z3 4.3

avoid old 'smt' method in examples