tuned signature;

clarified signature: replaced Sessions.Deps by Sessions.Structure from HTML_Context;

tuned;

clarified signature: avoid constants from Sessions.Structure within Session.Base;

clarified signature: avoid object-oriented HTML_Context; clarified theory_qualifier --- belongs to the overall Sessions.Structure;

tuned type signature

tuned type signature

streamlined theorems

more thorough split rules for div and mod on numerals, tuned split rules setup

streamlined simpset building, avoiding duplicated rewrite rules

consolidated attribute name

streamlined theorems

streamlined theorems and sections

streamlined primitive definitions for integer division

reintroduced SPASS to the mix

tweaked generation of Isar proofs

tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s

tuned comments;

updated to sumatra_pdf-3.4.6;

proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;

revived 'try0' and 'smart' Isar proofs in Sledgehammer

Cleanup of NonstandardAnalysis

A bit of cleaning up

The same, without adding a new simprule

moved some material from Sum_of_Powers

merged

clarified signature;

clarified theory_names with exported content;

proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);

proper treatment of empty lines (amending 08f89f0e8a62);

clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);

merged

The right way to formulate card_UNION, plus the old version for compatibility

tuned comments;

tuned signature;

clarified signature;

clarified signature;

clarified signature;

unused;

clarified modules;

clarified signature;

clarified signature: more explicit types;

clarified signature --- avoid dependent types;

tuned whitespace;

clarified signature: avoid public representation;

tuned signature;

clarified signature;

unused;

more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;

clarified signature: more explicit types; more robust zoom.factor: work with uninitialized GUI components;

tuned whitespace;

tuned, following 298707451ec2; tuned signature;

unused;

tuned, following hints by IntelliJ IDEA;

clarified signature: more explicit types; tuned whitespace;

tuned whitespace;

tuned, following hints by IntelliJ IDEA;

merged

more GUI elements;

clarified signature;

tuned;

tuned, following hints by IntelliJ IDEA;

clarified signature --- more operations;

clarified signature --- simplified types;

tuned signature;

proper toString for Content_XML, which is not covered by trait Content;

clarified output;

clarified signature: support different document_session, e.g. within running PIDE session;

unused (despite cf52379c0776);

tuned, following hints by IntelliJ IDEA;

unused (see 696819fe2424);

clarified signature;

basic setup for document build panel;

tuned, following hints by IntelliJ IDEA;

tuned, following hints by IntelliJ IDEA;

tuned;

clarified signature;

tuned, following hints by IntelliJ IDEA;

tuned, following hints by IntelliJ IDEA;

tuned signature;

tuned signature;

tuned signature, following hints by IntelliJ IDEA;

added support for cvc5 (whose interface is almost identical to CVC4)

removing the [simp] attribute breaks too many AFP entries severely

nlists is picked up automatically but conflicts with the RBT setup

new lemma

merged

New theory of fixed length lists

Further streamlining of quick-and-dirty evaluation.

more correct approximation (contributed by Achim Brucker)

Added tag Isabelle2022-RC0 for changeset b42e20adaeed

proper Java/Scala compiler classpath for standalone application (see also make_isabelle_app() in Pure/Admin/build_release.scala);

clarified message;

provide naproche-20220808 (inactive);

more robust data representation: notably for Store.read_session_timing with database_server;

tuned message;

afford default cache policy, despite 6a29709906c6;

tuned signature;

clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;

tuned;

tuned signature;

clarified signature;

clarified modules;

merged

tuned;

clarified message;

clarified signature: prefer Export.Session_Context over Sessions.Database_Context; discontinued obsolete operations;

clarified signature: prefer Export.Context;

clarified signature: find session_database within Session_Context.db_hierarchy;

clarified signature: prefer Export.Session_Context;

prefer Export.Context/Session_Context/Theory_Context over Sessions.Database_Context;

clarified signature;

tuned signature, following hints by IntelliJ IDEA;

clarified signature: more robust treatment of server;

discontinued Export.Provider in favour of Export.Context and its derivatives; uniform treatment of all sessions, including Pure;

clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;

tuned signature: more operations;

misc tuning and clarification;

clarified Document.Snapshot.all_exports: refer to material from this (virtual) session; clarified treatment of Session_Context.theory_names, added export_names; clarified treatment of document_snapshot: sites on top of the session_stack;

clarified database query: refer to semantic theories;