tuned imports;

always explore all sessions;

optionally explore all sessions -- potentially slow, e.g. for AFP;

proper sections;

clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;

proper base name, e.g. relevant for Code_Namespace.hierarchical_program;

clarified session graph: collapse theories from other sessions;

more robust error (amending 2c27c3d1fd3b): responsibility is gradually moved from ML to Scala;

exclude theories from other sessions; clarified modules;

some documentation;

actually qualify theory names;

merged

prefer formal name from session context, for proper qualified theory name;

clarified: Map index uses canonical files;

tuned signature;

tuned signature;

uniform use of theory base name for presentation;

proper imports_base, notably for thy_deps;

tuned signature;

tuned;

tuned GUI;

obsolete;

more uniform thy_deps (like class_deps), see also c48d536231fe;

special theories are always global;

tuned signature;

tuned signature;

tuned signature;

more systematic treatment of polynomial 1

consistent session name

more rules concerning of_nat, of_int, numeral

for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness

early abort on depth limit

obsolete

tuned

merged

clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";

clarified directories;

tuned signature (again);

proper bootstrap base for building Pure;

tuned according to Scala version;

more global theories;

tuned;

clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;

global session_base for PIDE interaction;

more explicit jEdit file operations; less redundant JEdit_Resources.node_name();

early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;

tuned;

tuned

more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function

merged

more informative known_files: known_theories within the local session directory come first; more thorough Session.Base.platform_path;

less global theories -- conflict with AFP entries;

support for known theories files (according to multiple uses);

proper display_name;

clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);

tuned signature;

proper import qualifier for global theories; clarified uniqueness;

explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;

proper qualifier for imports;

clarified, according to Scala version;

tuned text;

clarified signature;

NEWS;

more robust: user could provide name with "/" etc.;

clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;

added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;

clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;

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