merged

clarified empty merge; tuned;

permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make;

prefer native platform x86-windows, to make this work on x86_64-cygwin;

tuned signature;

even more robust syntax (amending 122df1fde073);

clarified error for bad session-qualified imports;

clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;

merged

completion supports theory header imports; tuned;

clarified modules;

tuned signature;

new theorem at_within_cbox_finite

process ROOT files only once, which allows duplicate (or overlapping) session root directories;

prefer Cygwin64, although some components still require update;

updated test version;

more recent polyml-test version;

misc tuning and modernization;

discontinued obsolete 'files' in session ROOT;

prefer file dependencies wrt. specific theories;

added command 'external_file';

proper document (cf. 9f5bfef8bd82);

removed pointless dependencies: done by 'spark_open';

merged

more documentation;

clarified imports: prefer parent session images;

eliminated old-style no-document imports;

proper document;

more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;

more documentation;

tuned;

sources_stamp refers to full sources; simplified data storage (again);

option -S for "isabelle build";

persistent storage of imported_sources;

cache sources: invoke SHA1.digest at most once; maintain imported_sources, as required for new theories;

tuned;

repaired small incident

updated SMT certificates and added one test

updated NEWS

properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)

option -B for "isabelle build" and "isabelle imports";

more standard merge operation;

updated Sledgehammer docs

added veriT component

more and updated documentation;

more and updated documentation;

discontinued rudiments of BSD support; tuned comments;

tuned;

NEWS;

x86-cygwin for tools is no longer supported;

updated to x86_64-cygwin;

updated to x86_64-cygwin;

auto update;

"windows" application is always x86_64;

merged

unused;

more accurate node_syntax: avoid overall_syntax for PIDE edits;

tuned signature;

clarified theory syntax vs. overall session syntax;

unused;

more informative loaded_theories: dependencies and syntax;

tuned signature;

tuned;

tuned signature;

tuned;

session-qualified theory names are mandatory;

discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;

eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen

Merge (resolved trivial conflict)

New results for Green's theorem

merged

merged

merged

merged

more proof simplificaition

merged

maintain loaded_files for each theory;

clarified: more uniform results;

slightly more parallelism;

prefer sequential file-system access, but parallel parse;

tuned;

clarified pure_files, based on uniform loaded_files;

tuned;

tuned signature -- more readable output as Scala value;

more operations;

strengthened reconstruction tactic

basic support for x86_64-cygwin;

Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen

back to post-release mode; updated package;

merged

Added tag Isabelle2017-RC3 for changeset 4f73201b8043

updated component: static build of for x86-linux, using actual cvc4 1.5 (see also c41642bc1ebb);

updated CVC4 and E components with 32-bit Linux and rebuild 64-bit Linux binaries

updated screenshots;

misc tuning and updates for release;

avoid duplicate message for @{action} in particular (see also @{action} within Pure);