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.

tuned proofs;

tuned;

double flush to ensure persistent "state" output is reset; tuned GUI;

reverted 2abbe7d700e9: "state" output is not necessarily proof state;

clarified default (again) in accordance to with Output dockable, despite more CPU resources requirements;

more thorough update of options;

limit statistics, to avoid exhaustion of heap space or GUI time;

render snapshot.is_outdated in text overview, where other status information is shown already;

avoid flashing of main text area (visual "grey-out") due to spurious edits, e.g. State panel auto-update;

clarified default;

recovered auto update from f9aaca00be49;

less intrusive rendering, notably for State dockable;

clarified rendering of Markup.DOC: like Markup.PATH / Markup.URL;

more direct access to option "editor_output_state";

tuned;

speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;

Now just a few seconds faster

merged

tuned

Theory of homotopic paths (from HOL Light), plus comments and minor refinements

merged

tuned

explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory

tuned;

tuned whitespace;

trim lines for @{theory_text} similarly to @{text};

tuned;

tuned and converted to cmp

misc. changes to Imperative-HOL from Peter Gammie

Refine the supression of abbreviations for morphisms that are not identities.

Merge

New theorems mostly from Peter Gammie

make SML/NJ happy;

converted to cmp

moved lemmas

derive lemmas uniformly

Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths

converted lookup to cmp

removed lemmas that were only needed for old version of isin.

clarified contexts by factoring out reading and definition of mixins

merged

export internal definition

corrected inefficient implementation

more tracing in MaSh

tuned names

NEWS

formally correct context for export

merged

merged

option "inductive_defs" controls exposure of def and mono facts;

tuned message;

added pretty syntax

tuned white space

leftover from 27ca6147e3b3

tuned whitespace

NEWS

droppen diagnostic junk from 4b53042d7a40

represent both algebraic and local-theory views on locale interpretation in interfaces