generalized generation of coinduction goal (towards nonuniform codatatypes)

export ML functions (towards nonuniform codatatypes) + signature tuning

export ML function

more uniform div/mod relations

proper logical constants

prefer existing logical constant over abbreviation

dropped aliasses

removed dangerous simp rule: prime computations can be excessively long

emphasize dedicated rewrite rules for congruences

moved and exported tactic

export ML function (towards nonuniform datatypes)

generalized ML function (towards nonuniform datatypes)

generalized ML function (towards nonuniform datatypes)

merge

renamed confusing variable names

clarified module name;

more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;

clarified module name;

merged

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

tuned;

$HOME/.bashrc provides TZ for *all* processes, resulting in proper date for Build_Log.log_date in remote_build_history via ssh (see also fe8f8f88a1d7);

trim more thoroughly, e.g. trailing \0 seen on some system;

tuned;

build sha1 library;

proper CONFIG_SITE for msys;

clarified platform selection;

more robust Windows platform;

copy libgmp on Linux;

prefer raw Admin tool, without Isabelle settings environment;

clarified command-line;

no backup of generated stuff;

more precise environment (for Windows);

proper shell_path for msys inside cygwin;

support other bash executable (notably for msys on Windows);

proper options; simplified command-line; tuned;

build_polyml in Scala;

clarified File.move: target directory like File.copy;

more logging, to see better when files written;

proper cleanup;

uniform order for options and args;

more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();

tuned comment;

proper option for "build", not "build_history" (cf. 5ca4ac099e94);

tuned;

simplified main proof;

misc tuning and modernization;

recovered Output.writeln for remote build_history (cf. ed8940d6295c), in order to have log files copied and removed;

more uniform path syntax, as in ML (see 5a7c919a4ada);

unused since 15865e0c5598;

added Nunchaku component and tuned Nunchaku integration accordingly

back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;

Added tag Isabelle2016-1-RC2 for changeset 2bf4fdcebd49

more robust multithreading;

documentation of @{undefined} (actually introduced in Isabelle2016);

tuned;

Scala "\u" notation uses hexadecimal, not octal (amending 00a135c0a17f);

HOL-Probability: fix import path in Fin_Map

disable CVC4 statistics, and hence crashes upon user interruptions

back to stable scala-2.11.8;

self_update of components, e.g. for vmnipkow9;

updated to scala-2.12.0;

tuned

more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');

extra newline as for other tools;

prefer standard_path for bash arg;

ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala);

proper remote repository source;

clarified setup_repository: even more uniform pull vs. clone (see also e84cba30d7ff);

pull isabelle-release;

Merged natlog2 into Discrete.log

moved IMP/Abs_Int_ITP to AFP/Abs_Int_ITP2012

added lemma