proper reset of column (amending 01e50039edc9);

added option -T: text length encoding;

more systematic text length wrt. encoding;

tuned;

more systematic text length;

unused;

proper counting of chars;

tuned;

clarified modules;

clarified modules;

tuned;

merge

generalized code (towards nonuniform datatypes)

clarified modules;

basic support for VSCode Language Server protocol; minimal extension for VSCode editor;

misc tuning and modernization;

tuned whitespace;

added isabelle jedit -R; errors in session_info/session_content are ignored and deferred to later checks of Build.build;

misc tuning and modernization;

more standard notation (like infix);

dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);

expose stderr, e.g. Multithreading.tracing;

test parallel proof terms in this small session (somewhat slow for bigger applications);

tuned messages -- more symbols;

tuned;

more permissive syntax; more PIDE markup;

reoriented congruence rules in non-explosive direction

more fine-grained type class hierarchy for div and mod

restructured matter on polynomials and normalized fractions

streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat

tuned fact references

clarified library contents

standardized notation

redundant

renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b

added lemmas demanded by FIXMEs

dropped comment after conversation with author: predicate compiler works independently from any code generator setup

unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;

tuned signature -- suppress pointless exports;

tuned;

more standard pretty printing; tuned messages;

tuned;

tuned whitespace; tuned comments;

refactored induction principle generation code, for reuse for nonuniform datatypes

merged

consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;

tuned signature -- more abstract type thm_node;

tuned signature;

tuned;

back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);

simplified options;

more careful derivation_closed / close_derivation;

always close derivation, for significantly improved performance without parallel proofs;

tuned whitespace;

removed of_string_limited;

tuned;

tuned;

tuned;

updated CASC instructions + tuning

support THF1 parsing for 'tptp_...' commands (e.g. 'tptp_isabelle') -- useful for CASC, SystemOnTPTP, ...

only recognize maps if the type names match

robustness

more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;

more symbols;

merged

removed obsolete RC tags;

Added tag Isabelle2016-1 for changeset 7aa3c52f27aa

tuned;

proper session HOL-Types_To_Sets; NEWS; CONTRIBUTORS; tuned whitespace;

Added tag Isabelle2016-1-RC5 for changeset 964ac7439a52

notes on whitespace;

avoid spurious messages -- potential cause of problems for "meson";

avoid spurious messages;

clarified output: avoid confusion with line:column notation;

clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);

updated Poly/ML repository test version (08-Dec-2016);

remove typo in bij_swap_compose_bij theorem name; tune proof

filter non-matching prems to not fail in proof procedure; include test case (related to c8a93680b80d)

more lemmas

spelling

misc tuning and modernization;

back to isabelle-dev repository;

merged

more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');

tuned;

merged

more lemmas, tuned proofs

don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful

added lemma about 'mult', as suggested by Bertram Felgenhauer

tuned proof

merged

Added tag Isabelle2016-1-RC4 for changeset 49708cffb98d

NEWS for e6a3c55b929b;

embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;

avoid extra space intruding rail diagrams (amending 4854f7ee0987);

explicit option editor_generated_input_delay, which is more aggressive by default;

clarified NEWS concerning Library/Poly_Deriv

made MaSh faster and less likely to hang seemingly forever

delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;

Added tag Isabelle2016-1-RC3 for changeset 51be997d0698

op powr for quickcheck[approximation] (amending 67792e4a5486)

skip over inner syntax for indentation;

tuned whitespace;

tuned;

more on "Indentation";

more on "Formal scopes and semantic selection";

misc tuning and updates;

more on JVM heap space;

tuned;

more on Isar proof language;

documentation for Isabelle/Scala tools; tuned;

more symbols;

avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;

more cronjob tasks, using Poly/ML repository version from 13-Nov-2016;

optional component setup;

clarified msys root; proper copy_files;

clarified setup: avoid alternative C compiler tools, e.g. from Homebrew or MacPorts;

proper admin tool;

tuned output;

back to regular Isabelle tool (reverting abc34a149690);