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;

more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;

remove sums_seq, it is not used

update syntax of has_*derivative to infix 50; fixed proofs

unify syntax for has_derivative and differentiable

tuned proofs

tuned internal construction

a few new theorems

proper flags for main action (amending 638b29331549);

tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;

merge semantic and syntax completion; tuned;

tuned;

tuned signature;