added lemmas, tuned spaces

entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless;

more informative Imports.Report with actual session imports (minimized);

more robust: allow URLs;

more robust: allow Windows file names;

clarified signature;

relaxed assm

back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);

reactivated unfinished tool (cf. a3a847c4fbdb);

tuned whitespace;

clarified meta_digest;

tuned;

added isablle build option -f;

canonical multiplicative euclidean size

clarified parity

clarified uniqueness criterion for euclidean rings

tuned proofs

tuned imports

fixed markup

ignore isolated nodes by default;

merged

cycle check with informative error;

tuned: each session has at most one defining entry;

more operations;

tuned signature;

tuned signature;

Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems

Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.

merged

tuned: less oo-non-sense;

operations for graph display;

tuned signature;

dependencies of entries vs. sessions; json output like "isabelle afp_dependencies"; misc tuning;

some administrative support for AFP;

tuned;

clarified signature: public access to ROOT file syntax;

euclidean rings need no normalization

more fundamental definition of div and mod on int

one uniform type class for parity structures

generalized some rules

avoid variant of mk_sum

adjusted implementation according to comment

dropped duplicates

generalized simproc

replaced recdef were easy to replace

elementary definition of division on natural numbers

tuned structure

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

Polynomial_Factorial does not depend on Field_as_Ring as such

avoid name clashes on interpretation of abstract locales

avoid trivial definition

canonical introduction and destruction rules for pairwise

avoid fact name clashes

spelling and tuned whitespace

tuned

fundamental property of division by units

removed mere toy example from library

tuned proofs

dropped dead code

Fixed the theorem name "closed_imp_fip_compact"

new material about connectedness, etc.

more on Docker;

removed obsolete RC tags;

build_docker is regular tool (non-admin);

merged

Added tag Isabelle2017 for changeset 64b47495676d

obsolete;

more NEWS;

updated for release;

merged

proper File.platform_path for SML/NJ on Windows;

clarified signature;

proper output of raw ML;

theory qualifier is always session name (see also 31e8a86971a8);

clarified session structure;

discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;

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);

more on indentation;

clarified "purge": retain .aux files etc. before "isabelle document", to allow 'document_files' providing such generated files (see also c3ea910b3581, 38ce936acb99);

clarified signature according to Scala version;

updated version for release;

proper result type (cf. b9f5cd845616);

recode Unicode text on the spot, e.g. from copy-paste of output;

support for workspace edits;

store document version;

auto update;

updated imports;

more documentation; tuned message;

more derived actions, according to jEdit/org/gjt/sp/jedit/gui/DockableWindowFactory.java;

proper tool name (cf. c1410bcf6e87);

proper standard_path to revert platform_path in JEdit_Sessions.session_base;

avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings);

clarified messages: after writing all files (see also 27f90319a499 and 57c85c83c11b);

spelling

clarified signature: proper result;

tuned;

document incompatibility

real oracle

Using the "constant_on" operator

added lemmas

two new simp rules

added lemma

added lemma; zip_with -> map2

introduced zip_with

added lemma

clarified signature: proper result;

new theorem about exposed faces

back to post-release mode -- after fork point;

tuned;

Added tag Isabelle2017-RC2 for changeset e9d8ff531700

tuned;

updated for release;

tuned headers;

Lawrence Paulson's contributions

merged

Correction of typos and a bit of streamlining

listed contribution

Simplicial complexes and triangulations; Baire Category Theorem

updated for release;

removed obsolete session

more robust backend identification

correctly locate SMBC from Nunchaku

added/updated components

tuned whitespace in Nunchaku output

eliminate artifact of translation in printed Nunchaku model

nicer numeral output for nats and ints in Nunchaku

rephrased error

tweaked Nunchaku bounds

speed up proofs slightly

use right attribute separator in Nunchaku

parse length-0 enums as well in Nunchaku

extended and renamed Nunchaku's Kodkod bounds

repaired Nunchaku cache handing

added Kodkod-specific options to Nunchaku

tuning

better model parsing and display in Nunchaku

properly parenthesize copy types in Nunchaku

proper Bash escaping

more precise output for Nunchaku

added singular 'solver' option to Nunchaku

got rid of unsound and needless beta-reduction in Nunchaku frontend

tuned Nunchaku's output

updated parser for Nunchaku irrelevant output

use proper syntax with nunchaku tool

moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years