tuned signature -- prefer qualified names;

more qualifier treatment, but in the end it is still ignored;

tuned signature;

provide Resources.import_name in ML, similar to Scala version; reset default_qualifier for now; tuned;

clarified;

more session_base information in ML; tuned signature;

more operations;

tuned signature;

merged

doc for comp. ind.

tuned signature

tuned headers;

merged

refer to known_theory; support for qualified theory name;

tuned;

provide session base for "isabelle build" and "isabelle console" ML process;

tuned comment;

more explicit lookup of loaded_theories: base names allowed here; no base names for known_theories;

support for all_known_theories of all sessions;

tuned;

known_theories from imported sessions;

tuned;

more checks;

tuned;

tuned signature;

tuned;

support for static session imports, without affect build hierarchy;

explicit Sessions.Selection;

more general signature; works for all terms, not just frees

session containing computational algebra

more approproiate placement of theories MiscAlgebra and Multiplicate_Group

clarified signature: tree structure is not essential;

merged

misc tuning and modernization;

merged

use Item_Net to store inductive info

tuned whitespace;

tuned signature;

more accurate qualified lookup; tuned;

clarified fall-back name;

tuned signature;

tuned whitespace;

clarified modules;

clarified checks -- avoid duplicated messages (amending 60c159d490a2);

proper default (amending 601866c61ded);

Fixed import path in Factorial_Ring

Merged

Merged

Tuned

Merged

moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series

moved material from AFP to distribution

merged

misc tuning and modernization;

uniform import_name, with treatment of global and qualified theories;

tuned signature;

more concise criterion

tuned

more on lists

store totality fact in function info

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;