Summary
- 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