updated documentation;

support multiple sessions, with cumulative errors; tuned command usage;

support regex patterns on messages;

support Pretty.unformatted, similar to ML version;

removed odd TODO item (see 3391a493f39a);

tuned signature;

tuned output: more Pretty.item;

tuned signature;

clarified failure: warning for logical error, exception for program breakdown;

print goal instantiation for global qed (and variations);

clarified output;

more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);

clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);

updated to postgresql-42.5.0;

tool to build Isabelle component for PostgreSQL JDBC;

clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";

option "show_states" for more verbosity of batch-builds;

tuned --- avoid warnings;

proper antiquotations;

inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;

proper antiquotations;

clarified options, following e.g. "show_consts";

proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;

unused (see 15758fced053);

clarified modules;

show goal instantiation, notably for 'schematic_goal' command (inactive by default);

proper umlauts;

tuned signature;

tuned signature;

tuned;

tuned;

tuned error message;

merged

merged

moved antimono to Fun and redefined it as an abbreviation

moved mono and strict_mono to Fun and redefined them as abbreviations

clarified generic euclidean relation

added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number

tuned signature;

check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";

tuned signature;

tuned --- more robust syntax;

tuned signature;

back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";

unused (see 347ed6219dab);

tuned signature;

more CONTRIBUTORS + NEWS;

tuned;

proper description;

tuned whitespace;

option "sort_updates" for record update simproc. Make proper record simproc definitions.

Merge

Three new theorems about real polynomial functions

tuned GUI;

tuned;

clarified GUI behaviour;

eliminated odd Unicode blanks;

tuned whitespace;

eliminated DOS line endings;

eliminated tabs, assuming tab-width=8;

eliminated tabs, assuming tab-width=4;

updated to current Cygwin, near 3.3.5-1;

test macOS 12 Monterey via laramac01;

clarified GUI update;

clarified signature;

tuned signature;

more GUI functionality;

clarified signature;

clarified component structure, concerning initialization order;

update VSCodium 1.65.2 ~> 1.70.1, Electron 13.5.2 ~> 18.3.5, Node.js v14.16.0 ~> v16.13.2;

provide cvc5-1.0.2 (inactive);

tuned output;

tool to build Isabelle component for cvc5;

tuned: avoid odd stateful programming;

more markup (for batch build);

tuned;

tuned;

tuned;

more NEWS;

updated some links;

more links, for files that formally belong to this session;

more links;

tuned antiquotations;

ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);

include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);

proper chapter_definition to prevent odd definitions by users;

tuned;

tuned signature;

proper order;

tuned whitespace for presentation;

clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in declaration order) vs. chapters (covered by visible sessions); clarified browser_info root index: preserve declaration order as much as possible;

clarified syntax: more uniform;

more robust, more strict;

tuned signature;

tuned;

tuned output;