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

assert Pure equations for theorem references; avoid dynamic reference to fact

assert Pure equations for theorem references; tuned

tuned specifications and proofs

merged

remove duplicate lemma finite_choice in favor of finite_set_choice

simplify proof

shorten some proofs

remove redundant simp rules ceiling_floor and floor_ceiling

misc tuning and simplification of proofs;

Document.removed_versions on Scala side;

discontinued predefined empty command (obsolete!?);

discontinued global execs: store exec value directly within entries; simplified entries: no extra copy of command_id;

Document.remove_versions on ML side;

some support to prune_history; clarified signature: recent_stable is supposed to be always defined;

merged

speed up extremely slow metis proof of Sup_real_iff (reducing total HOL compilation time by 5% on my machine)

remove redundant lemma reals_complete2 in favor of complete_real

simplify proof of Rats_dense_in_real; remove lemma Rats_dense_in_nn_real;

remove unused, unnecessary lemmas

remove more duplicate lemmas

merged

merged

avoid "Code" as structure name

more robust chunk painting wrt. hard tabs, when chunk.str == null;

raw message function "assign_execs" avoids full overhead of decoding and caching message body;

less agressive parsing of commands (priority ~1); join commands just before actual assignment;

tuned;

more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;

merged

Added Abstract Interpretation theories

tuned proofs;

proper config option linarith_trace;

discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;