tuned whitespace;

proper local_theory command;

more exports: avoid clones in AFP;

tuned;

export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files; tuned;

tuned whitespace;

merged

more informative Spec_Rules.Equational: support corecursion;

more operations;

more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.

merged

more informative Spec_Rules.Equational, notably primrec argument types;

clarified signature: avoid direct comparison on type rough_classification;

tuned proofs;

removed spurious debugging;

export propositional status of consts;

merged

generalised homotopic_with to topologies; homotopic_with_canon is the old version

follow up on Braun: get timing function right

Tweak Braun tree list_fast_rec recursion. A minor adjustment simplifies the termination argument slightly.

more robust: avoid NPE due to odd problems with object initialization;

RDF meta data for AFP entries; tuned;

more strict AFP properties;

tuned signature;

clarified signature;

proper treatment of empty extra lines (amending 98a440cfbb2b);

clarified signature: explicitly typed interfaces;

provide maintainers as seen in AFP/admin; suppress empty properties;

tuned;

tuned signature;