removed possible problematic dependency in HOL-Library.Multiset

HOL-Library: multisets of a given size

some facts about derivatives of products

more about formal convergence of power series

removed name clash in some lemmas

added orphaned theory to HOL-Analysis

some facts about power series

moved some lemmas to where they fit better

more efficient conversions for symbolic representations

notes on bit shift rewrites

explicit case rule

more lemmas

more lemmas

explicit check for computations on word type

more tidying

merged

tidied more proofs

removed duplicate lemmas

lots of lemmas for HOL, HOL-{Complex_}Analysis, HOL-Number_Theory

new lemmas for HOL-Complex_Analysis; overhaul of isolated_zeros

official theory for using bit shift operations for ordinary arithmetic if feasible

corrected operation

tuned whitespace

Simplified old proofs

merged

update to recent MSYS2 / MinGW, which also works via Cygwin;

tuned

tuned

tuned

tuned

revamped generation of functions

NEWS

typo

tuned

merged

Tidied some proofs

merged

clarified signature: more uniform;

tuned;

more accurate MinGW path conversion: support locations outside of mingw.root; uniform treatment of GMP, including Windows;

tuned messages;

tuned;

more uniform directory structure: Windows DLLs are treated like binaries;

tuned messages;

more uniform make_polyml_gmp vs. make_polyml;

clarified options: explicit use of existing GMP library;

clarified default options: prefer GMP from source;

Tidied more messy old proofs

more tidying and simplifying

merged

tidying some old proofs

Generalised a lemma and added another

merged

more robust;

more robust;

clarified GMP build options, notably for Windows;

more robust access to GMP library that is provided here;

clarified command-line;

tuned;

tuned;

more uniform verbose mode;

more explicit build stages;

tuned;

more uniform platform_context.execute;

more robust shell script;

tuned comments;

A couple of new lemmas

merged

clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);

clarified signature: fewer warnings in IntelliJ IDEA;

tuned: prefer explicit Bash.exports;

tuned signature;

clarified signature: more explicit type Platform_Context;

added option -G to build GMP library from sources;

Another Eberl lemma plus tidying

Another of Manuel's theorems

merged

More of Manuel's material

removed iprover from try0 because its name is clashing with iProver in Sledgehammer

expanded Sledgehammer's schedule (loosely inspired by "Hammering without ATPs" evaluation)

added try0's schedule to sledgehammer's schedule

clarified signature

clarified variable names

tuned

use existing implementations of bit operations if nat is implemented by target-language integer

merged

more comments;

mandatory option --enable-ho (see also fc5f10691147);

update to e-3.2, which is actually 3.2.5; enforce rebuild of Isabelle/ML;

reflect nested lists in variables names

Simplified lemma (as suggetsed by Stepan Holub)

incorporate target-language integer implementation of bit shifts into Main

represent constants with explicit typargs to avoid false positives for equality approximations like ‹card UNIV === card UNIV›

restored type reconstruction for nbe: remaining type variables must remain schematic for checking

tuned

merged

NEWS;

more documentation;

update jedit component;

more navigator positions;

clarified navigator events: avoid excessive 0 positions;

more robust: make double-sure that get_text does not crash (see on non-existent file);

more uniform treatment of open buffer vs. loaded file (NB: setCaretPosition includes selectionNone);

proper hyperlink column (amending 6898054035d6);

tuned: setCaretPosition already includes selectNone;

tuned signature;

clarified history: eliminate pointless var _current;

clarified target position: line start + offset (or column); more uniform treatment of open buffer vs. loaded file;

tuned source structure;

eliminated patch: imitate jEdit.gotoMarker more directly;

tuned;

tuned signature: proper private vars;