tuned comments

simplify proof of Bseq_mono_convergent

merged

replace lemma expi_imaginary with reoriented lemma cis_conv_exp

remove redundant lemmas expi_add and expi_zero

remove redundant lemmas about LIMSEQ

introduce abbreviation 'int' earlier in Int.thy

remove unused assumptions from natceiling lemmas

move lemmas nat_le_iff and nat_mono into Int.thy

eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);

simplified signatures;

synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;

tuned document;

improved handling of extended styles and hard tabs when prover is inactive;

mark hard tabs as single chunks, as required by jEdit;

updated READMEs;

property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;

moved XML/YXML to src/Pure/PIDE; tuned comments;

pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);

pseudo-definition for perms on sets; tuned

remove duplicate lemma nat_zero in favor of nat_0

merged

merged

modify nominal packages to better respect set/pred distinction

merged

remove unused assumption from lemma posreal_complete

tuned specifications

merged

tuned proof

merged