refactored some HORRIBLE integration proofs

merged

improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann

tuned code setup

strengthened tactic

Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike

strengthened tactic (for 'fun' BNF)

new material: Colinearity, convex sets, polytopes

poles and residues of the Gamma function

merged

new derived targets for evaluating Haskell and Scala programs

Printing natural numbers as numerals in evaluation

fmap is finite

facts about cardinality of vector type

Adapted Approximation_Bounds to changes in Multiset

Simprocs for roots of numerals

Updated NEWS

HOL-Analysis: Infinite products

More material on powers for HOL-Computational_Algebra/HOL-Number_Theory

additional lemmas for State_Monad, courtesy of Andreas Lochbihler

more material on finite maps

redundant since c6714a9562ae

store the unfolded definitions of the lifted bnf constants under "_def" name

state monad

State_Monad ~> Open_State_Syntax

more material on fmaps

canonical representation for fmaps is fmlookup

fmaps are countable

merged

card_0_eq ~> fcard_0_eq

material from $AFP/Formula_Derivatives/FSet_More

FSet is monadic

finite sets are countable

lift sum to finite sets

tuned

clarified

dropped superfluous theory imports

revised lemma

merged

generalized lemma

proper check wrt. distinct entry dates;

added lemma

some generalizations complex=>real_normed_field

proper concept of code declaration wrt. atomicity and Isar declarations

merged

complete on long name components as well;

added command 'alias' and 'type_alias';

tuned;

tuned signature;

unused;

qualify Complete_Partial_Order2.compact

tuned;

proper fonts (cf. 1d219d76873b);

all_known can cause timeout of VSCode server startup, notably on Windows;

tuned documentation; updated package version; updated screenshot reference;

clarified screenshot;

NEWS;

tuned;

more documentation;

retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;

clarified platform file operations;

more operations;

clarified signature;

more robust: always package;

prefer explicit link;

updated package;

provide --baseImagesUrl for VSCode extensions marketplace;

tuned;

updated package;

tuned;

added screenshot;

clarified;

updated package;

tuned;

tuned output;

tuned spelling;

more documentation;

auto update;

clarified editor focus;

proper hyperlink_command, notably for locate_query; support bidirectional caret update;

tuned signature;

proper dynamic controls, notably for auto_update_enabled;

tuned signature;

HTML GUI actions via JavaScript;

more operations/options;

clarified signature;

merged

support for HTTP/POST method; more explict type HTTP.Arg;

clarified defaults;

tuned signature;

auto update;

added missing files (cf. 5aa9cb83e70e);

auto update;

GUI controls similar to Tools/jEdit/src/state_dockable.scala;

GUI layout similar to Pure/GUI/wrap_panel.scala;

Removed more "guess", etc.

more error checking

merged

some HTML GUI elements;

proper bootstrap_name (amending b42743f5b595);

clarified indentation;

More tidying of horrible proofs

A few renamings and several tidied-up proofs

back to scala-2.12.2, after a41435469559;

more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char

treat "undefined" constants internally as special form of case combinators

Improved error reporting when activating a locale instance (beyond syntax decls).

Additional corollary Knaster_Tarski_idem_inf_eq.

clarified indentation;

clarified indentation;

merged

tuned signature;

tuned;

NEWS;

indentation of keywords after input;

indent = 0 for blank lines: produce less whitespace by default;

clarified prev_line: stop at blank line;

more information;

tuned signature;

tuned;