clarified modules;

tuned;

clarified message;

clarified signature;

tuned -- use zero-based Line.Position;

VSCode already detects URLs from plain text;

clarified signature;

tuned signature;

tuned signature -- more explicit types;

basic support for hyperlinks / Goto Definition Request;

clarified border cases;

tuned messages;

proper pattern match;

more explicit error;

more explicit error;

display messages, according to regular Isabelle Output;

tuned;

clarified node_name: preserve original uri;

clarified directories;

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;