tuned;

clarified signature;

clarified components;

avoid name clash

avoid name clash

lemma

tuned;

another example for lift_bnf for quotients

adapted to LuaLaTeX according to Isabelle/299f6a8faccc;

merged

more robust init: avoid spilling opam artifacts;

proper \usepackage[T1]{fontenc};

proper type-setting of cartouches (requires T1);

more robust;

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

obsolete (see 0c837beeb5e7);

removed unused latex packages;

proper Isabelle/Scala tool --- avoid perl;

generalized confluence-based subdistributivity theorem for quotients;

Backed out changeset b867b436f372

Backed out changeset 3fdb94d87e0e

Only check for libffi if we are building the interpreted version.

reduced dependencies on List_Permutation

follow corresponding precedence on sets

reduced dependencies on List_Permutation

follow corresponding precedence on sets

consolidated names

reduced dependencies on theory List_Permutation

consolidated names

reduced dependencies on theory List_Permutation

obsolete (see f3378101f555);

merged

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

more direct unlimited smt_timeout;

clarified timeouts in Isabelle/ML;

tuned --- more elementary Time operations;

obsolete;

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

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

Fix offset of RBX in "memory register" array. Needed for callbacks in 32-in-64.

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

typo

tuned

merged

added upper bound on monomorphisation duplicate instances

tuned exec field in atp_config

tuned best_slices in atp_config

tuned proofs;

removed junk;

clarified compiler options: show relevant warnings;

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

clarified signature --- fewer warnings;

clarified signature --- fewer warnings;

tuned --- avoid compiler warnings;

tuned --- fewer warnings;

more robust ordering (see also 88c96e836ed6);

proper scala.collection.immutable;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

more robust error;

tuned --- fewer warnings;

tuned --- fewer warnings;

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

tuned --- fewer warnings;

Tuned presentation of Buffon's needle

slightly more efficient Term.fastype_of (only little impact in regular…

tuned

reduced dependencies on theory List_Permutation

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 --- silence odd warning;

tuned --- fewer warnings;

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

tuned --- avoid deprecated Predef.any2stringadd;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

download more directly, via means of JVM;

clarified signature, according to Isabelle/Scala;

download on separate thread;

clarified signature;

tuned;