allow to load this into "isabelle jedit -l HOL";

print like syntax of Thy_Header.header;

more explicit types;

proper name according to meaning;

more main sessions and global theories;

eliminated redundant imports;

eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;

tuned (see also 1fa1023b13b9);

tuned header;

tuned signature;

proper base name;

tuned;

tuned syntax; some official documentation;

clarified: allow to qualify theories from ROOT;

refer to global_theories from all sessions, before selection;

tuned signature;

tuned;

macbroy30 is on 10.12 Sierra (already since 04-Mar-2017) -- discontinued support for 10.8 Mountain Lion;

back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";

tuned headers;

proper imports; tuned headers;

tuned message;

merged

misc tuning and modernization;

clarified imports;

tuned signature;

tuned;

provide session qualifier via resources;

proper qualifier (again, see df4cd6e1fdfa);

simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);

tuned;

tuned signature;

removed problematic simp rule

merged

tuned

Merged

added shuffle product to HOL/List

tuned

added chains of (in)equations

misc tuning and modernization;

misc tuning and modernization;

clarified YXML vs. symbol encoding: operate on whole message; tuned signature;

clarified YXML vs. symbol encoding: operate on whole message;

tuned proofs;

misc tuning and modernization;

tuned signature;

tuned

more lemmas

tuned proof;

merged

misc tuning and modernization;

support to encode/decode command state; support to merge full contents of command state;

tuned;

more operations;

tuned signature;

eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);

Corrected affiliation.

updated to jedit-5.4.0;

misc tuning and modernization;

clarified signature: rowid is specific to SQLite;

proper primary key;

more general primary_key;

tuned;

more operations;

tuned;

proper SQL syntax (according of PostgreSQL);

access table via session_name: db may in principle contain multiple entries;

more operations;

eliminated somewhat redundant inlined name (despite a7aa17a1f721);

more informative session result;

simplified signature (despite 448325de6e4f);

clarified signature;

tuned;

more realistic PIDE build session;

more uniform options;

asynchronous send_stop operation;

more process arguments;

proper message text (see also fa62e095d8f1);

support PIDE option (inactive); misc tuning;

more explicit build_session args; support both command-line and PIDE version;

avoid compiler warning;

actually throw exception;

clarified result;

reset print_mode, e.g. relevant for saved heap;

clarified init (see also 32755e357a51, ac48def96b69);

restore output channels after shutdown, e.g. relevant for saved heap;

clarified signature;

merged

tuned;

proper columns;

tuned signature;

more general signature: not limited to SQLite;

suppress inlined properties from log output;

prefer database, but also accept log.gz from historic versions;

more robust JDBC initialization, e.g. required for Isabelle/jEdit startup;

maintain persistent session info in SQLite database instead of log file;

tuned;

tuned signature;

tuned;

tuned message;

clarified signature;

more selective queries;

clarified data representation;

data representation with XML.Cache; tuned;

clarified name;

SQL database operations for combined session info;

prefer non-strict default;

clarified signature (again, see also 3ed43cfc8b14);

tuned signature;

tuned;

tuned comments;

clarified message: exception output usally happens in a context without extra newline;

Removed [simp] status for Complex_eq. Also tidied some proofs

Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.

always output proof state: there is only one output buffer in Isabelle/VSCode;

updated package;

merged

unused;

misc tuning and modernization;

clarified message;