tuned signature;

more operations for profiling;

provide rsync component, with uniform version + options on all platforms;

tuned message;

provide local component to remote directory;

tuned output;

more SSH operations;

more operations;

tuned comments;

clarified directory names, following bash_process (see e59d7d6fe1bd);

tuned README;

clarified build options;

more portable options;

build rsync from sources, to avoid divergence of protocols on various platforms;

more informative errors;

clarified options;

tuned messages;

provide Isabelle tool wrapper;

more robust errors: proceed updating database; clarified options; clarified progress;

tuned;

tuned output;

clarified signature;

clarified modules;

tuned comments (amending 1951f6470792);

tuned;

discontinue somewhat pointless is_single, which also depends on details of internal data representation;

more compact data: approx. 0.85 .. 1.10 of plain list size; fewer comparisons for Leaf2 / Leaf3: observe order;

slightly more compact data;

more operations, notably for profiling;

tuned;

more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain list;

tuned --- fewer compiler warnings;

tuned;

tuned;

tuned;

tuned signature: more uniform structure Key;

prefer Sortset.T for shyps;

tuned;

more operations;

tuned names: "e" means "entry" in table.ML and "elem" in set.ML;

NEWS;

added Set.size; tuned Set.merge: keep larger set stable;

performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;

performance tuning: prefer functor Set() over Table();

efficient representation of sets: more compact than Table.set;

tuned whitespace;

tuned comments;

tuned signature;

clarified signature;

tuned signature;

tuned output;

removed junk (amending 236e43c8bb5b);

tuned;

tuned output;

tuned performance: much faster low-level operation;

clarified signature: more general operation Bytes.read_slice;

clarified signature: more explicit types;

clarified signature: more explicit types;

clarified signature: more explicit types; tuned output;

More explicit type information in dictionary arguments.

tuned

tuned whitespace

more uniform approach towards satisfied applications

more uniform approach towards satisfied applications

tuned

tuned

Tuned semicolons.

reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element

added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element

refactored proofs

added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element

reversed import dependency between Relation and Finite_Set; and move theorems around

more operations;

clarified theory_sizeof1_data: count bytes, individually for each data entry;

clarified operations for ML object sizes;

merged

simplified a lot of messy proofs

merged

added lemma multp_repeat_mset_repeat_msetI

more operations;

merged

merged

Proof simplification

proper "build_thorough" for "isabelle update" (amending 9e5f8f6e58a0);

merged

back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;

vacuum everything in the database;

tuned;

proper vacuum of session_info tables: only once per build process;

tuned signature;

more thorough database checks;

more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;

clarified build options;

clarified ML option vs. Scala option (see also caa182bdab7a);

merge conflict

unified function update and map update syntaxes

removed accidental junk

map update syntax

proper sorting of result (amending f458547b4f0f);

merged

enforce rebuild of Isabelle/ML;

more operations;

more specific vacuum operation, which is also relevant to PostgreSQL;

tuned signature: removed redundant argument;

tuned signature;

proper build_uuid for Build_Process.Task: thus old entries are removed via prepare_database/clean_build;

more informative Build_Process.Snapshot;

more explicit snapshot of "_state" and "_database";

tuned;

removed redundant State.workers: directly maintained within the database, using with SQL update;

more thorough cleanup;

tuned signature;

tuned signature;

tuned signature;

more thorough synchronization of internal "_state" vs. external "_database";

more database content; clarified signature;

clarified modules;

clarified signature;

clarified modules;

tuned output;

tuned output;

Adjusted to new map update priorities

bring priority in line with ordinary function update notation

merged

use tree (simpler) instead of rbt (exercise)

enforce rebuild of Isabelle/ML;

more direct state update;

avoid too many synchronized_database;

tuned output;

synchronize progress messages with database;

more robust SQL query for mandatory arguments;

synchronize progress stop/stopped with database;

more database content;

tuned whitespace;

tuned signature;

tuned whitespace;

clarified signature: avoid confusion due to object-orientation;

clarified modules;

clarified signature: prefer explicit types;

more accurate Sessions.Info.session_prefs: cover relative changes wrt. statically declared options;

clarified signature: more explicit type Options.Spec, which incorporates all variants of Options.+;

tuned output;

clarified signature: more explicit types;

clarified signature: prefer static types;

clarified signature (again, see also 8c64e51d9dde and 268bf61631ec);

tuned signature;

more operations, thanks to Jsoup;

discontinued apache-commons in favour of jsoup, which is smaller and more useful;

more accurate shasum_meta_info;

tuned signature;

support "isabelle options -l -t TAGS";

NEWS;

clarified signature;

tuned;

avoid hard-wired stuff (see also 78f2475aa126);

clarified tags;

clarified session prefs (or "options" within the database);

tuned signature;

tuned comments;

unused (see 268bf61631ec);

clarified exported options;

clarified signature;

do not export connection details (password etc.);

support option tags;

use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism

don't try to falisfy goals with schematics

enforce rebuild of Isabelle/ML;

more robust transactions;

proper support for Option[Date] columns;

more robust transactions;

clarified signature;

enforce rebuild of Isabelle/ML;

proper test (amending 32f9e75c92e9);

updated to sqlite-jdbc-3.41.0.0;

proper shasum lines (amending 3070001c9d1f);

more robust transactions;

explicit locking for PostgreSQL --- neither available nor required for SQLite;

merged

assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;

more database content, e.g. for monitoring;

tuned structure;

tuned signature;

more database content, e.g. for monitoring;

more explicit workers, e.g. for monitoring;

tuned;

tuned;

clarified worker state: always maintain database content via worker_uuid; clarified message;

clarified signature: prefer Build_Process.Context for parameters;

support for "isabelle build -j0": require external workers to make progress;

follow renaming of various Isabelle command-line tools (see b975f5aaf6b8 and before);

require the presence of free variables to do abduction in Sledgehammer

removed exercise solution

merged

new theory Tree_Rotations

proper tool name (amending cbb49fe8e5a2);

proper file-name (amending b975f5aaf6b8);

tuned headers;

eliminated suspicious Unicode characters;

tuned whitespace;

renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");

renamed administrative tools to build Isabelle components (unrelated to "isabelle build");

renamed "isabelle build_components" to "isabelle components_build" (unrelated to "isabelle build");

sort lines;

renamed "isabelle log" to "isabelle build_log";

clarified structure;

tuned output;

clarified signature: proper abstract type;

clarified signature: support all arguments of Sessions.store();

tuned;

basic setup for "isabelle build_worker";

tuned comments;

tuned structure;

clarified terminology of "session build database", while "build database" is the one underlying Build_Process;

clarified modules;

clarified signature: reduce boilerplate;

clarified messages;

tuned signature;

tuned structure;

clarified signature;

clarified signature;

clarified build process roles: "worker" vs. "build";

clarified database content; tuned signature;

tuned: prefer iterator.nextOption;

tuned whitespace and braces;

clarified signature: more uniform operations;

tuned signature: reduce boilerplate;

tuned signature;

proper clean_build of old data at start of new process --- allow to inspect remains of the last process;

more database content: formal end_build;

more operations;

clarified database content and prepare/init stages;

tuned signature;

tuned;

tuned;

less verbosity, amending 3bc49507bae5;

tuned comments; tuned structure;

tuned signature: avoid totally adhoc overriding;

separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;

enforce rebuild of Isabelle/ML, after various changes to build database management;

more detailed table "isabelle_build_serial": allow to monitor activity of build_process instances;

tuned output;

clarified database content: store actual value instead of index;

more robust: disallow override;

tuned messages;

more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;

clarified signature: manage "verbose" flag via "progress";

removed unused arguments: avoid ambiguity concerning progress/verbose;

clarified protocol for "verbose" messages;

clarified signature: manage "verbose" flag via "progress";

tuned;

tuned;

more operations;

tuned signature;

more robust: proper bound checks;

enforce rebuild of Isabelle/ML, after various changes to build database management;

clarified modules;

clarified signature: manage "verbose" flag via "progress";

clarified treatment of "verbose" messages, e.g. Progress.theory(); always store messages within database, with explicit "verbose" flag: client-side will decide about output;

proper "val verbose" (amending 2e2b2bd6b2d2);

tuned whitespace;

more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);

support progress backed by database; moved Build_Progress.Context.progress/log to class Build_Process: database is available here;

tuned;

tuned messages;

clarified signature: require just one "override def echo(message: Progress.Message): Unit";

tuned signature;

tuned signature;

clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";

proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;

merged

more database content; clarified signature; tuned comments;

tuned signature;

tuned whitespace;

tuned signature;

merged

More of Eberl's material

Some new lemmas. Some tidying up

detect duplicates in Sledgehammer output -- suggested by Larry Paulson

got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)

merged

clarified execution context: main work happens within Future.thread; clarified signature: only one "join" operation;

clarified timeout: closer to actual process;

tuned names;

clarified names;

tuned, following ML_Statistics.monitor;

unused (see also 0cebcbeac4c7);

tuned;

tuned;

tuned comments;

clarified modules; tuned signature; tuned comments;

clarified modules;

clarified modules;

clarified signature;

clarified modules;

clarified modules;

tuned;

clarified modules;

clarified modules;

tuned;

more robust: proper synchronization of transition from next_job to start_session;

more thorough synchronized_database for internal *and* external state;

simplified startup under "locked" condition (in contrast to f7e413e8d269);

more explicit session name, in anticipation of variants like "session.document", "session.browser_info";

tuned signature;

tuned signature;

tuned signature;

tuned signature: support general Build_Job instances;

tuned signature;

clarified signature: prefer static data;

tuned signature;

identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);

tuned signature;

tuned signature;

tuned signature;

tuned;

unused;

tuned signature (again);

tuned;

tuned;

proper deps from build_graph, not imports_graph (amending 0c704aba71e3);

misc tuning: more direct access to ancestors, without build_graph;

tuned signature (again);

clarified signature: reduce explicit access to static Sessions.Structure;

tuned signature;

clarified modules (again);

tuned;

tuned signature;

avoid premature Properties.uncompress: allow blob to be stored in another database;

more robust: synchronized access to database;

clarified signature: do not expose global state to object-oriented variants;

tuned comments and outline;

merged

Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed

A little bit more tidying up

tweaked Sledgehammer interaction

there won't be an E version 2.7

reverted 0506c3273814 -- the message is still useful

compile

adopt terminology suggested by Larry Paulson

more robust E proof parsing

avoid double 'Warning:' in Sledgehammer messages

tweaked abduction in Sledgehammer

slightly more documentation

renamed new Sledgehammer option

updated documentation

improve ad hoc abduction in Sledgehammer

tuning

don't apply abduction and consistency checking to goals of the form 'False'

implemented ad hoc abduction in Sledgehammer with E

tuned;

clarified scope of "serial" and "numa_index" within database;

clarified signature: allow more general init, e.g. from existing database;

clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;

tuned;

simplified somewhat pointless error message (see also 0189fe0f6452);

clafified signature: simplify object-oriented reuse;

revert pointless 375c6b9ce9ea: overall thread context is already uninterruptible (see 54ac957c53ec);

tuned whitespace;

merged

Fixed a presentation error

Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem

tuned whitespace;

tuned;

clarified signature, although "sql" argument is de-facto mandatory;

tuned;

proper SQL (amending 7ab9bac1ca96);

clarified signature: more explicit "synchronized" regions;

more robust interrupt handling, notably for Build_Job.terminate();

clarified signature: works for general Build_Job;

tuned;

clarified modules;

clarified signature;

proper log_lines, without protocol messages (amending cb3f5361fbca);

clarified signature;

tuned messages;

clarified error output vs. process_result stored in build_database (see also 13a0f537e232 and bff56eae3ec5);

clarified system option: guard for testing, until the database layout has stabilized;

merged

Simplified some proofs

clarified db content: avoid redundancy of historic ML_IDENTIFIER;

merged

proper filterNot, not filterNot-not;

option build_hostname allows to change hostname easily;

clarified permissions of build.db, following server.db;

enforce rebuild of Isabelle/ML, after various changes to build database management;

misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;

tuned: fewer warnings in IntelliJ IDEA;

clarified init_database vs. update_database: implicitly assume fresh "instance";

clarified Build_Process.Context: cover all static information;

tuned whitespace in generated SQL;

tuned: prefer typed operations;

clarified signature: more concise operations;

more robust options in "prefs" format: avoid odd control character;

proper settings for hostname: allow to adjust it in user space;

support for build database: still inactive; more detailed Build_Job.Node_Info;

tuned signature;

clarified signature: more robust operations;

tuned;

tuned;

more operations;

clarified signature: more operations;

clarified signature;

clarified signature: more robust (see also cf2ef4be3630);

unused (see also 7b318273a4aa and a1fb4d28e609);

tidying ugly proofs

brought back [...] maplet syntax

merged

has_sum now an infix operator!!

merged

New material contributed by Manuel

Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation

added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO

added lemma multpDM_plus_plusI[simp]

added lemmas multpDM_mono_strong and multpHO_mono_strong

merged

One new (necessary) theorem

merged

more operations to support management of jobs, e.g. from external database;

more uniform operations;

more operations;

clarified signature: more robust;

more operations;

allow arbitrary info, e.g. for custom scheduler;

clarified signature;

merged

Simplified some proofs

merged

tuned signature;

tuned signature: avoid warnings in IntelliJ IDEA;

tuned signature;

tuned signature;

tuned signature;

clarified state: more explicit type as plain value, which is also easier to sync with external db;

tuned signature;

tuned signature;

clarified signature: support meaningful subclasses for Build.Engine implementations;

support alternative build engines, via system option "build_engine";

misc tuning and clarification; support SSH.System;

proper test, following Platform.is_linux;

clarified signature;

clarified signature;

merged

Simplified some more proofs

merged

Replacing z powr of_int i by z powi i and adding new material from the AFP

merged

tuned: avoid redundant white space;

clarified signature: more robust operations, without assumption about node 0;

clarified signature: more concise operations;

clarified modules: NUMA is managed by Build_Process;

tuned signature;

clarified signature: move all parameters into Build_Process.Context;

clarified signature;

more elementary data structures, to fit better to SQL database;

clarified signature (see also 68a7ad1385bc);

clarified signature;

clarified modules; clarified signature;

merged

merge in backouts

Backed out changeset bafdc56654cf

backout rev 334015f9098e (for Main_Doc.thy only)

Backed out changeset 1fde0e4fd791

merged

Simplifying more proofs

merged

proper Nodes.init (amending 9b35c1171d9a);

unused;

tuned;

clarified signature defaults;

clarified types: support a variety of Build_Job instances;

clarified signature: more explicit synchronized operations;

clarified signature: more explicit synchronized operations;

clarified modules (again); clarified signature: idempotent "finish" operation, analogous to "join";

clarified signature: more explicit synchronized operations;

clarified signature: more explicit synchronized operations;

more robust: first register job, then start job;

clarified signature: proper scope of synchronized operation;

proper synchronized access to mutable state, to support concurrency eventually;

tuned signature: explicit marker for mutable global state;

tuned;

more robust;

clarified signature;

clarified modules;

merged

Tidied some really messy proofs

added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO

Simplified a few proofs

Moved up a theorem

Limit properties for complex exponential

More of Eberl's contributions: memomorphic functions

merged

New material due to Eberl on Formal Laurent Series

merged

A bit more tidying and some new material

removed rarely used error in Sledgehammer

merged

tuned

added refute mode to Sledgehammer to find 'counterexamples'

merged

Map.map_of movement

removed Map from docu

move map_of to List

updated NEWS

careful eta-contraction in Metis to keep argument to All and Ex expanded

merged

merged

clarified main operations; clarified main loop;

clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;

prefer global mutable state, in order to break up the loop eventually;

clarified modules;

clarified signature;

clarified static build_context vs. dynamic queue;

clarified signature: make dynamic Queue from static Context;

clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;

tuned;

tuned;

clarified data structure: use static info from deps, not dynamic results; tuned;

clarified data structure: more direct access to timeout;

tuned;

misc tuning and clarification;

clarified modules; clarified signature;

tuned message: old_time not sufficiently prominent nor accurate to be printed;

clarified signature and terminology;

clarified signature: avoid adhoc constants;

tuned;

tuned message;

tuned signature: more operations;

clarified signature: more explicit types;

clarified modules;

clarified signature;

clarified signature;

merged

Simplification of proofs

explicit range types in abstractions

somehow more clear terminology

tuned

Some basis results about trigonometric functions

merged

Even more new material from Eberl and Li

merged

More material for Analysis and Complex_Analysis

actually executable enum_all, enum_ex for word

tuned text

Lots of new material chiefly about complex analysis

merged

More new theorems from the number theory development

merged

proper orientation for right-associative operations;

tuned signature;

tuned signature;

tuned signature;

obsolete --- superseded by SHA1.Shasum operations;

clarified signature, using right-associative operation;

tuned whitespace;

tuned --- implicit split;

clarified signature;

prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;

tuned signature;

more uniform use of SHA1.Shasum;

proper Shasum.digest, to emulate old form from build_history database; clarified signature: more explicit types;

prefer explicit shasum; clarified signature;

proper symbolic dependencies, e.g. for Demo_FoilTeX;

prefer explicit shasum;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature;

Some more new material and some tidying of existing proofs

more diagnostic operations (see also 5c7652e9bc01);

more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);

clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);

tuned;

clarified modules;

tuned signature;

update to polyml-5e9c8155ea96, which is more robust on arm64;

more robust dependencies for Pure;

proper compiler root for arm64;

clarified "isabelle build_polyml": download and build everything for current platform; renamed former "isabelle build_polyml" to "isabelle make_poly", for experimentation and diagnosis;

no view_document after build: avoid loss of focus, especially in "auto build" mode;

tuned message;

build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;

clarified modules;

maintain document_output meta data;

clarified modules;

avoid redundant SelectionChanged events;

more logging;

proper symbolic handle on component resources: diff -r ci-extras-1/etc/settings ci-extras-2/etc/settings 1c1,4 < classpath "$COMPONENT/lib/ci-extras.jar" --- > #-*- shell-script -*- :mode=shellscript: > > ISABELLE_CI_EXTRAS_JAR="$COMPONENT/lib/ci-extras.jar" > classpath "$ISABELLE_CI_EXTRAS_JAR" diff -r ci-extras-1/README ci-extras-2/README 11a12 > Makarius, 02-Feb-2023

more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);

More of Manuel's material, and some changes

less verbosity by default, notably for regular "isabelle build -o document";

clarified message: old-style log is usually empty;

clarified messages, notably for session "Intro";

merged

more general program start message; progress on "Creating directory";

clarified terminology of inlined "PROGRAM START" messages;

isabelle update -u cite -l "";

less ambitious parallelism: avoid exhaustion of memory (40GB total);

clarified GUI;

clarified GUI: omit pointless search buttons, as real output is shown as markup;

more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant;

merged

More new material thanks to Manuel

merged

tuning

alternate AFP tests on lrzcloud2, to fit better into one day;

merged

support document preparation from already loaded theories;

clarified GUI events;

clarified GUIs: keep related buttons together;

proper program name, e.g. for session "Intro";

clarified GUI events: reset everything on session context switch;

clarified GUI events: ensure fresh output when switching pages;

clarified GUI: avoid odd jumping pages on "Cancel";

clarified GUI events;

more accurate output: avoid output_body from last run;

more accurate output: avoid output_main from last run;

removed unused operation from 3f50b24909df;

clarified guard: avoid spurious auto builds;

automatically build document when selected theories are finished;

more accurate Word.capitalize: do not touch name;

defer build until document nodes are ready;

clarified signature: prefer semantic status;

removed obsolete parameter (see 7c23db6b857b);

clarified Document_Editor.Session: more explicit types, more robust operations; eliminated await_stable_snapshot in favour of delay_build;

more operations;

clarified operation (without change of signature!);

pointless

Lots more new material thanks to Manuel Eberl

merged

Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl

observe option "show_states" in headless server (see also 951abf9db857);

text correction

enable clean_components by default: it saves a lot of local disk space, notably on virtual nodes;

merged

removed somewhat pointless support for Jenkins log files: it has stopped working long ago;

more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";

tuned signature;

more operations;

obsolete (see also d547173212d2);

clarified names to emphasize suble differences in meaning;

prefer high-level Other_Isabelle.bash over low-level SSH.execute;

unused (see 378bb7a739c3);

more options to manage resolved components;

proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);

tuned comments;

tuned;

clarified signature: more explicit types; scale chart output, instead of stored data;

more operations;

tuned;

clarified signature: more robust field_scale;

clarified signature: more explicit types;

clarified signature;

tuned;

support units, e.g. java.lang.Long.MAX_VALUE is 8 EiB;

more explicit types;

prefer typed/strict operations;

tuned message;

prefer strict operation: java.io.File.length returns 0 for non-existent file;

prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;

back to Scala 3.2.0 for now, since 3.2.1 causes odd crash of REPL concerning value classes (e.g. "isabelle.Time.now()"); enforce rebuild of Isabelle/ML + Isabelle/Scala;

Restored antiquotation.

tuned whitespace

merged

added lemma multpHO_plus_plus[simp]

Shortened a messy proof

Moved in some material from the AFP entry Winding_number_eval

merged

tuned messages: less verbosity;

prefer Other_Isabelle.init instead of adhoc scripts;

tuned message, following "isabelle components -a";

clean components more accurately: purge other platforms or archives;

more operations for SSH.System;

clarified signature;

tuned;

manage other Isabelle distributions via SSH;

more operations for SSH.System;

recovered option -C from 092449efcb0e (still required for isabelle_cronjob.scala on Windows), but with slightly different meaning;

clarified parameters (again);

Some new material from the AFP

clarified defaults: imitate "isabelle components -I" without further parameters;

tuned;

merged

more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;

tuned;

clarified defaults (see also b310b93563f6);

tuned comments;

discontinued adhoc change of environment (from 897f1ac84aab), following ssh c2e8ba15a10a;

more formal Other_Isabelle.settings, with derived expand_path / bash_path;

clarified signature: minimal interface for getenv/expand_env, instead of bulky java.util.Map;

tuned;

discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);

more operations;

removed unused user_home argument (see also 897f1ac84aab and 19b6091c2137);

tuned;

more robust: self-contained Other_Isabelle.isabelle_home;

more robust and uniform Other_Isabelle.scala_build;

tuned;

tuned message;

more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;

more strict;

tuned signature;

proper ssh.bash_path;

merged

added lemma irreflp_on_multpHO[simp]

added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and totalp_multpHO

Beautifying an old entry

generalized theory name: euclidean division denotes one particular division definition on integers

merged

support remote operations;

more elementary command-line, following lib/Tools/components;

clarified defaults; proper Url.append_path;

more accurate options (amending 7e19dc018db9);

clarified defaults;

support remote download_file;

more modular shell script;

more uniform options for "curl", following lib/Tools/components;

tuned: drop redundant "expand";

tuned;

added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp

proper name for lemma totalp_on_total_on_eq

update to jdk-17.0.6; proper executables for Windows; enforce rebuild of Isabelle/ML and Isabelle/Scala;

proper cleanup;

avoid odd suffix in published HTML library;

tuned signature: avoid aliases;

tuned message;