unused;

Merge

New complex analysis material

infix syntax for measurable set

more standard term equality;

tuned;

tuned signature;

tuned message;

merged

more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;

tuned;

clarified ML scopes; tuned;

clarified ML scopes;

tuned;

unused;

tuned;

clarified modules;

modernized

modernized

modernized

isabelle update_cartouches -c -t;

proper checksum for cygwin-20151210.tar.gz (some snapshot after 1.7.35-1);

avoid application spurious startup error;

current Cygwin snapshot in preparation of release;

hardwired LANG, to avoid sporadic surprises with local environments;

make SML/NJ happy;

not_leE -> not_le_imp_less and other tidying

clarified terminology

tuned;

tuned signature;

tuned signature;

tuned;

more direct use of Token.src as token list; tuned signature; tuned;

merged

unused;

merged

clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;

tuned;

tuned;

added Proof_Context.add_thms_dynamic, which is potentially useful for Eisbach;

sorted out eventually_mono

tightened invariant

isabelle update_cartouches -c -t;

Merge

Cauchy's integral formula for circles. Starting to fix eventually_mono.

Merged

Generalised derivative rule for division on formal power series

tuned;

more thorough update request: semantic state of command may have changed elsewise;

tuned signature;

tuned whitespace;

isabelle update_cartouches -c -t;

isabelle update_cartouches -c -t;

tuned;

tuned;

updated to polyml-5.6-20151206, which presumably improves stability on Windows;

discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;

added AA trees

tuned

tuned

avoid name clashes

added Brother12_Map

tuned docs

more documentation on 'size' plugin

nicer error when the given size function has the wrong type

merged

added 1-2 brother trees

updated SMT certificates

removed needless complication for modern SMT solvers

tuned language

moved section according to supposed order of interest

consolidated documentation

modernized

tuned sections

modernized

alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism

prefer conventional read/check distinction over manual check

clarified role of context for reading rewrite specifications

formally correct context for export, which got screwed up in 87203a0f0041

tuned whitespace

removed needless ML function

tuned whitespace

reverted inadvertently qfinished/pushed change r164eeb2ab675

merged

add formalisation of Bourbaki-Witt fixpoint theorem

add lemmas

strengthen lemma

Merge

Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.

set "transfer_rule" attribute more generously

tuned whitespace

misc tuning and modernization;

misc tuning and modernization;

tuned;

avoid 'hence' and 'thus' in generated proofs

removed tracing

RBT invariants for insert

removed junk;

merged

more reactive GUI;

tuned;

paint root black after insert and delete

observe option "indent";

more scalable GUI;

paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement); avoid hardwired colors (see 1d9c121cbe4d); updated to Highlight 2.2;

Ported old example to use (co)datatypes

discontinued Mac OS X 10.7 Lion (macbroy6);

merged

clarified font: GUI defaults might change dynamically;

updated platform baseline to Mac OS X 10.8 Mountain Lion;

updated to polyml-5.6-20151123;

Merge

New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.

bundle main sources read-only, to avoid accidental editing of imported theories etc.;

more symbols;

some GC options that potentially improve reactivity;

more thorough completion rendering, e.g. "Un";

tuned;

Updates to the revision history of the locales tutorial.

Clarify locale qualifiers: output and tutorial.