tuned signature;

Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems

Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.

merged

tuned: less oo-non-sense;

operations for graph display;

tuned signature;

dependencies of entries vs. sessions; json output like "isabelle afp_dependencies"; misc tuning;

some administrative support for AFP;

tuned;

clarified signature: public access to ROOT file syntax;

euclidean rings need no normalization

more fundamental definition of div and mod on int

one uniform type class for parity structures

generalized some rules

avoid variant of mk_sum

adjusted implementation according to comment

dropped duplicates

generalized simproc

replaced recdef were easy to replace

elementary definition of division on natural numbers

tuned structure

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

Polynomial_Factorial does not depend on Field_as_Ring as such

avoid name clashes on interpretation of abstract locales

avoid trivial definition

canonical introduction and destruction rules for pairwise

avoid fact name clashes

spelling and tuned whitespace

tuned

fundamental property of division by units

removed mere toy example from library