2017-04-19 wenzelm 2017-04-19 tuned imports;
2017-04-19 wenzelm 2017-04-19 always explore all sessions;
2017-04-19 wenzelm 2017-04-19 optionally explore all sessions -- potentially slow, e.g. for AFP;
2017-04-19 wenzelm 2017-04-19 proper sections;
2017-04-19 wenzelm 2017-04-19 clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
2017-04-19 wenzelm 2017-04-19 proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
2017-04-18 wenzelm 2017-04-18 clarified session graph: collapse theories from other sessions;
2017-04-18 wenzelm 2017-04-18 more robust error (amending 2c27c3d1fd3b): responsibility is gradually moved from ML to Scala;
2017-04-18 wenzelm 2017-04-18 exclude theories from other sessions; clarified modules;
2017-04-18 wenzelm 2017-04-18 some documentation;
2017-04-18 wenzelm 2017-04-18 actually qualify theory names;
2017-04-17 wenzelm 2017-04-17 merged
2017-04-17 wenzelm 2017-04-17 prefer formal name from session context, for proper qualified theory name;
2017-04-17 wenzelm 2017-04-17 clarified: Map index uses canonical files;
2017-04-17 wenzelm 2017-04-17 tuned signature;
2017-04-17 wenzelm 2017-04-17 tuned signature;
2017-04-17 wenzelm 2017-04-17 uniform use of theory base name for presentation;
2017-04-17 wenzelm 2017-04-17 proper imports_base, notably for thy_deps;
2017-04-17 wenzelm 2017-04-17 tuned signature;
2017-04-17 wenzelm 2017-04-17 tuned;
2017-04-17 wenzelm 2017-04-17 tuned GUI;
2017-04-17 wenzelm 2017-04-17 obsolete;
2017-04-17 wenzelm 2017-04-17 more uniform thy_deps (like class_deps), see also c48d536231fe;
2017-04-17 wenzelm 2017-04-17 special theories are always global;
2017-04-17 wenzelm 2017-04-17 tuned signature;
2017-04-17 wenzelm 2017-04-17 tuned signature;
2017-04-17 wenzelm 2017-04-17 tuned signature;
2017-04-17 haftmann 2017-04-17 more systematic treatment of polynomial 1
2017-04-17 haftmann 2017-04-17 consistent session name
2017-04-16 haftmann 2017-04-16 more rules concerning of_nat, of_int, numeral
2017-04-13 haftmann 2017-04-13 for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
2017-04-13 haftmann 2017-04-13 early abort on depth limit
2017-04-13 haftmann 2017-04-13 obsolete
2017-04-13 haftmann 2017-04-13 tuned
2017-04-13 wenzelm 2017-04-13 merged
2017-04-13 wenzelm 2017-04-13 clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
2017-04-13 wenzelm 2017-04-13 clarified directories;
2017-04-13 wenzelm 2017-04-13 tuned signature (again);
2017-04-12 wenzelm 2017-04-12 proper bootstrap base for building Pure;
2017-04-12 wenzelm 2017-04-12 tuned according to Scala version;
2017-04-12 wenzelm 2017-04-12 more global theories;
2017-04-12 wenzelm 2017-04-12 tuned;
2017-04-12 wenzelm 2017-04-12 clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;
2017-04-12 wenzelm 2017-04-12 global session_base for PIDE interaction;
2017-04-12 wenzelm 2017-04-12 more explicit jEdit file operations; less redundant JEdit_Resources.node_name();
2017-04-12 wenzelm 2017-04-12 early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;
2017-04-12 wenzelm 2017-04-12 tuned;
2017-04-12 haftmann 2017-04-12 tuned
2017-04-12 haftmann 2017-04-12 more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function
2017-04-12 wenzelm 2017-04-12 merged
2017-04-11 wenzelm 2017-04-11 more informative known_files: known_theories within the local session directory come first; more thorough Session.Base.platform_path;
2017-04-11 wenzelm 2017-04-11 less global theories -- conflict with AFP entries;
2017-04-11 wenzelm 2017-04-11 support for known theories files (according to multiple uses);
2017-04-10 wenzelm 2017-04-10 proper display_name;
2017-04-10 wenzelm 2017-04-10 clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
2017-04-10 wenzelm 2017-04-10 tuned signature;
2017-04-10 wenzelm 2017-04-10 proper import qualifier for global theories; clarified uniqueness;
2017-04-10 wenzelm 2017-04-10 explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
2017-04-10 wenzelm 2017-04-10 proper qualifier for imports;
2017-04-10 wenzelm 2017-04-10 clarified, according to Scala version;