merged

uniform proof of lemmas

merged

adapt to 90f54d9e63f2

add various lemmas

add lemmas

generalise lemma

add lemmas for extended nats and reals

add various lemmas

cancel complementary terms as arguments to sup/inf in boolean algebras

add lemmas about monoids and groups

tuned

recovered from a9c0572109af;

merged

tuned whitespace;

added @{command}, @{method}, @{attribute};

smart quoting of non-identifiers, e.g. jEdit actions;

more thorough check_action, including completion;

tuned signature;

clarified modules;

more thorough check_command, including completion;

clarified modules;

unused;

ignore pointless/unused options;

added document antiquotation @{theory_text}; tuned document;

allow open symboloid;

generalized so that is also works for veriT proofs

fixing premises in veriT proof reconstruction

Merge

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

subdegree/shift/cutoff and Euclidean ring instance for formal power series

prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply;

uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;

qualifier is mandatory by default;

prefer explicit State panel;

suppress already persistent state output as well;

added option timeout_scale;

syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML;

clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);

tuned;

less confusing markup;

added @{undefined} with somewhat undefined symbol;

ML cartouches via control antiquotation;

more formal treatment of control symbols;

more antiquotations;

more antiquotations;

retain traditional rendering of \<paragraph>;

added glyphs 0x204b, 0x2b1a from DejaVuSansMono;

tuned;

tuned

tuned

updating options to verit

isabelle update_cartouches -c -t;

isabelle update_cartouches -c -t;

IsabelleText for unusual symbol;

isabelle update_cartouches -c;

merged

Convertd to 3-way comparisons

isabelle update_cartouches -c;

symbolic syntax "\<comment> text";

avoid ligatures;

added propertional dashes from DejaVuSans (not Mono): 0x2013, 0x2014, 0x2015;

tuned whitespace;

tuned whitespace;

tuned whitespace;

updated;

more antiquotations;

document antiquotation @{footnote}; render \<^footnote> as pilcrow -- the rarely used \<paragraph> loses its interpretation;

dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;

eliminated Nitpick's pedantic support for 'emdash'

tuned;

NEWS;

Keyword 'rewrites' identifies rewrite morphisms.

Qualifiers in locale expressions default to mandatory regardless of the command.

merged

tuned signature;

prefer Isabelle/Scala Future;

prefer Isabelle/Scala Future;

tuned imports;

more direct task future implementation, with proper cancel operation; more uniform Future.thread;

tuned;

prefer ad-hoc non-worker threads;

clarified modules;

cancel already running request;

added acknowledgement in Binomial.thy

Merged

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

don't pollute local theory with needless names

allow selectors and discriminators with same name as type

make sure that function types are never generated as '> @ A @ B', but always as 'A > B'

merged

avoid premature flushing and thus flashing of text area;

tuned whitespace;

clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);

redundant;

tuned whitespace;

tuned document;

tuned document;

tuned document;

isabelle update_cartouches -t;

avoid highlighted area getting "stuck" after edit;

clarified completion of Isabelle symbols within document source;

more accurate imports: allow re-uses of base names in PIDE interaction (amending 60c159d490a2);

merged

tuned names and optimized comparison order

updated CVC4 component to deal with paths with whitespace

Merged

Rounding function, uniform limits, cotangent, binomial identities

merged

back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;

global start time as reference point;

tuned signature -- clarified modules;

obsolete (see 9c6346319eee, 7924d61b50cf);

added splay trees

added many small lemmas about setsum/setprod/powr/...

no icons here -- not a standalone window;

workaround for problem with C-1, C-2, C-3 seen on Slovak QWERTY keyboard;

removed presumably obsolete workaround (see 7924d61b50cf);

Cauchy's integral formula, required lemmas, and a bit of reorganisation

merged