more thorough checks of browser_info file conflicts;

tuned;

prefer strict operations with explicit errors (instead of missing HTML output);

more thorough check, without path name artifacts (e.g. "./README");

tuned signature; tuned messages;

clarified signature: Sessions.Base_Info follows Sessions.Base;

clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);

tuned;

tuned whitespace;

evade clash with index.html (allow "Index.thy" even on case-insensitive file-systems);

discontinued special support for README.html (which was hardly ever used in the past 2 decades);

clarified directory layout (again): mimic original directory layout, notably ISABELLE_HOME;

more robust treatment of Document.Node.Name, following stored data;

more robust;

clarified directory layout: files are relative to enclosing theory;

tuned signature: avoid duplication;

more robust: theories could have been suppressed via option "condition";

tuned signature;

tuned messages (again, see d50c2129e73a): presentation setup could fail initially for take some time;

clarified modules;

clarified signature: support for adhoc file types;

clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory; distinguish Nodes.Theory.static_session vs. dynamic_session: refer to exports from dynamic_session, corresponding to strictly to build_graph; more robust treatment of source files and links to generated files; retrieve entities by their file position, within its corresponding session/theory hierarchy;

export entity file position as well, e.g. relevant for HTML presentation with aux. files;

proper permissive = true (amending 475fedc02737)

tuned signature;

clarified signature;

clarified signature;

more robust directory structure: always relative to session_dir; tuned messages;

discontinued slightly odd integrity check (from af2d0e07493b): requires a different approach;

clarified signature;

misc tuning and clarification;

unused;

tuned signature;

tuned signature;

tuned signature;

clarified modules;

clarified modules;

unused;

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