clarifed module name;

tuned proofs;

clarified module arrangement; more antiquotations;

clarified modules; more antiquotations for antiquotations;

more antiquotations;

clarified bootstrap process: switch to ML with context and antiquotations earlier;

more markup for improper elements;

tuned signature;

unused;

tuned signature -- rearranged modules;

tuned proofs;

back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828); more explicit shutdown;

remove unnecessary finiteness assumptions from lemmas about setsum

adapt to Isabelle/c726ecfb22b6

fix HOL-NSA; move lemmas

cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}

changed policy when to define constants

tuned proofs; removed duplicated facts

additional lemmas

removed dependencies on theory Ordered_Euclidean_Space

use cbox to relax class constraints

merged

tuned;

more antiquotations;