Topology_Euclidean_Space.thy: organize section headings

simplify some proofs

generalize lemma convergent_subseq_convergent

locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses

locale-ize some constant definitions, so complete_space can inherit from metric_space

generalize constant 'lim' and limit uniqueness theorems to class t2_space

Quotient Package: make quotient_type work with separate set type

updated README;

touch descendants of edited nodes; more precise handling of Graph exceptions;

parellel scheduling of node edits and execution;

tuned error message;

retrieve imports from document state, with fall-back on theory loader for preloaded theories; misc tuning;

explicit check of finished evaluation;

refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;

simplified exec: eliminated unused status flag;

consistently use variable name 'F' for filters

generalize lemmas about LIM and LIMSEQ to tendsto

HOL-Nominal-Examples: respect distinction between sets and functions

less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;

merged

HOL-Hahn_Banach: use Set_Algebras library

ex/Quickcheck_Examples.thy: respect distinction between sets and functions

clarified Toplevel.end_theory;

simplified Toplevel.init_theory: discontinued special name argument;