clarified errors;

tuned signature;

tuned;

merged

reverted the substitution here

merged

fixed some remarkably ugly proofs

de-applying and tidying

follow Phabricator update 2020 Week 37;

clarified defaults for nitpick;

tuned nitpick message: more like quickcheck;

clarified;

evaluate Scala via running Isabelle/Scala;

more robust: avoid spurious line breaks that might confuse the scala interpreter;

clarified signature: proper eval/print via interpret;

clarified name;

factored out typedef material

tuned;

tuned;

tuned;

proper platform_path for Windows;

evaluate PolyML via running Isabelle/ML;

output via file instead of stdout;

proper context;

clarified signature;

tuned signature;

tuned

more thorough treatment of division, particularly signed division on int and word

canonical enum instance for word

merged

clarified signature;

proper ml_source: avoid duplicate Bash.string;

misc tuning and clarification: prefer functions over data;

tuned;

misc tuning and clarification;

tuned messages;

tuned;

merged

de-applying and simplifying

tuned

removal of needless premises

merged

de-applying

dropped junk

typo

NEWS and CONTRIBUTORS

integrated generic conversions into word corpse

more lemmas

added lemma

de-applying

merged

merged

cleaned up some messy proofs

prefer current mathpartir.sty from underlying TeX distribution;

more checks;

more uniform color --- avoid odd transparency on Windows (due to jEdit default #666699a);

updated documentation;

tuned documentation;

clarified modules;

more uniform JVM vs. ML status widget;

clarified modules;

update to official jedit-5.6.0;

merged

tidying and de-applying

restructured

tuned theory structure

more on conversions

generalized signed_take_bit

more on conversions

generalized

a bit of tidying

merged

de-applying

discontinue export_document --- always enabled (reverting f0f83ce0badd);

unused (see also 7b318273a4aa);

tuned proofs;

proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);

a new lemma

more informative bibtex errors;

merged

minor tidying, also s->S and t->T

more on conversions

merged

quite a bit of tidying

more robust interpretation of data;

merged

small quantifier fixes

just a bit of streamlining

but not the [cong] rule

tidying up some theorem statements

initial Kodkod.warmup: preloading and basic integrity test;

strict init of protocol handlers;

clarified treatment of add-on prover_options;

clarified signature;

clarified modules;

tuned;

clarified signature;

tiny tidy-up of proofs

updated to scala-2.12.12;

updated to polyml-test-a3cfdf648da: performance improvements for GC statistics;

NEWS;

test HOL-Nitpick_Examples with Isabelle/Scala instead of external process: much faster;

updated to kodkodi-1.5.6: more robust treatment of interrupt;

removed pointless version checks: Isabelle component integration does the job already;

more robust treatment of execution with interrupts; tuned comments;

suppress odd warning for context.exit();

more explicit treatment of interrupt;

tuned;

more flexible default for max_threads;

proper default for max_threads; proper warmup example;

a proof of concept for generic conversions

proper name (amending 742d94015918);

invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);

avoid odd PIDE markup, notably in kokodi input;

clarified names;

clarified signature;

clarified signature;

proper treatment of timeout: <= 0 means already timed out, but for $KODKODI/bin/kodkodi it would mean NO timeout;

proper treatment of absolute deadline vs. relative timeout;

clarified session: no parent image for minor theory imports;