clarified signature: more explicit HTTP operations;

tuned;

more robust;

clarified signature;

clarified components;

avoid name clash

lemma

tuned;

another example for lift_bnf for quotients

merged

proper \usepackage[T1]{fontenc};

more robust init: avoid spilling opam artifacts;

proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;

provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;

more robust; eliminated perl;

removed unused latex packages;

obsolete (see 0c837beeb5e7);

proper Isabelle/Scala tool --- avoid perl;

generalized confluence-based subdistributivity theorem for quotients; new example that triggered the generalization

Backed out changeset 3fdb94d87e0e

Backed out changeset b867b436f372

reduced dependencies on List_Permutation

follow corresponding precedence on sets

consolidated names

reduced dependencies on theory List_Permutation

obsolete (see f3378101f555);

merged

more direct unlimited smt_timeout; update of certificates: generated command-line options are part of input / digest;

clarified smt: support Timeout.ignored and Timeout.scale_time;

clarified timeouts in Isabelle/ML;

tuned --- more elementary Time operations;

removed unused/pointless operation: Time.start is the load/init time of this Scala module;

obsolete;

clarified signature --- augment existing structure Time;

rebuild SMT certificates from scratch;

added lemmas (sublist|prefix|suffix)_list_all

added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While

added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI

typo

merged

added upper bound on monomorphisation duplicate instances

tuned best_slices in atp_config

tuned exec field in atp_config

removed junk;

tuned proofs;

enforce full build, after significant changes in Isabelle/Scala;

clarified compiler options: show relevant warnings;

tuned --- avoid compiler warnings;

clarified signature --- fewer warnings;

clarified signature --- fewer warnings;

tuned --- fewer warnings;

more robust ordering (see also 88c96e836ed6);

proper scala.collection.immutable;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

more robust error;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);

slightly more efficient Term.fastype_of (only little impact in regular applications);

reduced dependencies on theory List_Permutation

Merge

reverted simprule status on a new lemma

merged

tiny bit of lemma hacking

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- avoid deprecated conversions between certain number type;

tuned --- avoid deprecated Predef.any2stringadd;

tuned --- silence odd warning;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

clarified signature, according to Isabelle/Scala;

download more directly, via means of JVM;

download on separate thread;

clarified signature;

tuned;

proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);

tuned signature;

NEWS

lemma diffusion

more connections between mset _ = mset _ and permutations

dissolve theory with duplicated name from afp

more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;

more Isabelle/ML/Scala operations;

more Isabelle/ML/Scala operations;

more Isabelle/ML/Scala operations; clarified errors;

proper src1, amending 20157c8ab3f3;

tuned;

proper File.eq, amending df49ca5da9d0;

tuned;

clarified modules: more like ML;

obsolete;

tuned;

more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);

discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;

more checks;

clarified message;

clarified message;

clarified comments;

clarified message;

improved list_neq simproc

merged

repaired document

merged

merged

A couple of basic lemmas about arg

multiset as equivalence class of permuted lists

emphasize connection to multisets

proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work;

more on Isabelle_System.bash;

more specific name