more lemmas

include GCD as integral part of computational algebra in session HOL

prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);

added missing file (amending f533820e7248);

theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;

merged

clarified parent session images, to avoid duplicate loading of theories;

tuned;

removed pointless document;

moved lemmas from AFP to Isabelle

moved lemmas from AFP to Isabelle

two new induction principles on multisets

merged

clarified session imports;

clarified standard_import: based on Known.get_file as in PIDE editors;

afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;

proper imports_resources for import_name: avoid self-referential name resolution;

more precise position information;

tuned imports;

proper "~~" backup as documented;

clarified: explicit check of result;

clarified imports;

clarified local_theories: exclude ancestor sessions;

more standard master_dir;

eliminated default_qualifier: just a constant;

more uniform isabelle_scala; more uniform ISABELLE_SCALAC_OPTIONS with heap options;

include imports that morally belong to Main and are used in HOL-Proofs applications;

tuned;

proper theory_qualifier;

more global theories;

actual update_imports operations;

more operations;

tuned signature;

more operations;

tuned signature;

tuned whitespace;

clarified;

store Sessions.Info.name;

wrapper for "isabelle update_imports" with selection options like "isabelle build";

more position information;

removed French accent from docs

removed Old_SMT legacy module

typo

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);