explicit type class operations for type-specific implementations

obsolete

added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran

merged

generalized type

basic setup of Isabelle setup tool --- pure Java, no dependencies;

merged

guess package more directly;

merged

Just one lemma

proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;

clarified platforms;

merged

proper jEdit.props (amending ff716ecb0805);

update to gmp-6.2.1, with support for arm64-darwin;

clarified platforms;

clarified options: implicitly support both x86_64 and arm64;

tuned whitespace;

centralized more lemmas

avoid Fun.swap

guide is out of focus

proper build for fresh target directory (amending d9823224fcfe);

put more resources into jedit_build component;

more brackets (see f6b453449cc6);

more brackets;

proper settings variable, amending 6e85281177df;

merged

tuned proofs --- avoid z3, which is absent on arm64-linux;

proper condition: z3 could be absent, e.g. on arm64-linux;

build auxiliary jEdit component in Isabelle/Scala; clarified directory layout;

separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);

tuned message;

clarified signature;

tuned signature;

more elementary swap

tuned comments;

misc updates and clarification;

clarified file name;

merged

updated to polyml-5.8.2 (official release);

clarified default_platform_families (again);

proper option for linux_arm;

proper "$?";

proper jvm_platform, notably for org.sqlite.lib.path;

tuned message;

support for platform family "linux_arm";

clarified purge;

removed junk;

support local build_heaps; more robust build_release;

merged

tuned --- rename = dist_name is sufficient;

proper dist_name;

clarified option -P: allow empty argument;

support for existing release archive; misc tuning and clarification;

tuned signature;

clarified signature;

more website content;

misc tuning and clarification: more explicit types Release_Context, Release_Archive;

tuned signature;

tuned theory structure

more appropriate location

collected lemmas on permutations

A nice cardinality lemma

tuned

more robust indentation: proper line context after insert;

more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();

support nested cases;

tuned;

tuned;

early definition of ML antiquotations;

tuned;

clarified signature: more operations;

clarified signature: more operations;

clarified signature;

tuned signature;

clarified command-line, following other build_XYZ tools;

more recent OCaml and GHC stack: better support for Apple Silicon;

merged

avoid "exec" to change the winpid;

clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);

fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);

clarified signature;

rebuild executable for x86_64-darwin;

clarified command-line;

update Linux base-line;

tuned comments;

tuned signature;

simplified typesetting of \<guillemotleft>...\<guillemotright>;

collecting more lemmas concerning multisets

proper use of antiquotations;

more documentation on "Conversions";

tuned

updated example;

clarified options (again);

more options: update ISABELLE_IDENTIFIER;

clarified conditional ML;

support for conditional ML text;

updated example;

clarified options;

proper context variable handling when stripping leadings quantifiers from test goals

proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);

eliminated perl: prefer elementary GNU printenv;

more robust bootstrap of components;

more self-contained support for macOS;

misc tuning and clarification;

tuned signature;

support for base64 via Isabelle/Scala/ML;

compile;

clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);

clarified signature (again);

merged

clarified signature;

unused;

unused;

clarified signature: more structured arguments, notably for remote provers;

clarified signature;

clarified signature: avoid tmp file;

clarified signature for Scala functions;

clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);

tuned;

clarified cache;

clarified signature: Bytes extends CharSequence already (see d201996f72a8);

clarified exceptions;

more uniform use of Byte_Message; support protocol_message with multiple chunks;

tuned signature;

tuned signature;

more robust treatment of empty markup: it allows to produce formal chunks;

collected combinatorial material

tuned;

tuned;

more documentation;

proper treatment of nested antiquotations; clarified signature;

support for ML special forms: modified evaluation similar to Scheme;

clarified signature: more detailed token positions for antiquotations;

merged

clarified signature;

confluent preprocessing for floats in presence of target language numerals

subclass relation

some tinkering with npm versions;

some tinkering with npm versions;

back to post-release mode;

tuned signature;

auto-update due to "isabelle build_vscode";

tuned;

tuned --- following hints by IntelliJ IDEA;

fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)

simplified definition

new lemmas

discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove";

following recent Phabricator update, after 2021 Week 13 (Late March);

merged

Cosmetic: no !! in the lemma statement

clarified README; avoid odd patching of sources;

more standard header, with utf-8 encoding;

clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;

merged

new automatic order prover: stateless, complete, verified

clarified signature;

clarified: follow "isabelle version -t";

further clarification of Isabelle distribution identification -- avoid odd patching of sources;

tuned signature -- more explicit types;

more robust and uniform ISABELLE_TAGS;

clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;

simplified release status (again), in contrast to a43898f76ae9;

more uniform HTTP resources;

clarified (again): local tip could be actually more recent;

tuned;

tuned;

clarified name;

more systematic java_library: avoid empty entries, declaration order as for other bash functions;

support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;

updated to latest latex due to new mechanism for dealing with bold ccfonts

removal of needless hypothesis in hd_rev and last_rev

more robust;

clarified message;

tuned;

tuned message;

proper export;

more options: build is part of default setup;

misc tuning and clarification;

more options;

proper Admin script, outside the settings environment;

tuned whitespace;

tuned;

clarified;

tuned message;

tuned message;

more accurate settings after update of current version;

clarified messages;

more robust: lest hg work out remote tip; more options;

more options;

clarified treatment of multiple versions: last one counts; more options;

more robust;

more robust: explicit repository root;

more robust;

more convenient repository setup;

tuned;

more robust invocation of hg;

more robust: idempotent;

more robust invocation of hg;

tuned;

clarified output; more options;

support repository archives (without full .hg directory);

more robust invocation of hg;

record official releases that follow a certain structure, with public access via https://isabelle.sketis.net/repos/isabelle/raw-file/tip/Admin/Release/official (NB: Isabelle2013-1 had to be retracted);

dedicated session for combinatorial material

support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;

enforce full build;

turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;

discontinue fragile check in LaTeX, e.g. problems with toc entries;

merged

merged

type class relaxation

more NEWS;

clarified group (but hard to tell);

more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd; corresponding symbols and latex macros;

more lemmas

clarified package name (actually both pxfonts and txfonts exist and have this font);

tuned;

prefer isabelle bbbfont;

enforce full build;

clarified symbol names, notably relevant for Z_Notation;

update README (actually after update of component);

high-quality blackboard-bold fonts from "txmia" (package "txfonts");

publish component;

further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;

clarified \<Zcomp> (small) vs. \<Zsemi> (big);

more CONTRIBUTORS;

more Z_Notation symbols, as proposed by Simon Foster; some LaTeX-art based on tex.stackexchange "How do you make a square element symbol (\in)";

more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus";

clarified order for GUI panel;

prefer more direct interpretation

more Z_Notation symbols, as proposed by Simon Foster;

more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt;

clarified order for presentation in isar-ref (Appendix B);

prefer explicit \<Zproject> (with its own Unicode codepoint);

more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster; NB: no bold version of 0x2900 due to fontforge crash "Internal Error: Some fragments did not join";

tuned message;

proper directory of settings file; tuned;

tuned lemma

added lemma

tuned signature;

tuned signature (again);

tuned --- following hints by IntelliJ;

tuned comments;

proper shell quote;

removed spurious references to perl / libwww-perl;

invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl); clarified inlined command-line; clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function);

clarified signature: refer to file name instead of file content;

compile;

clarified signature: more explicit types;

support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;

clarified signature;

elapsed time to download content (and for the server to provide content);

more direct elapsed run_time via bash_process wrapper (via Scala and C);

merged

use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;

clarified signature: let Sledgehammer handle SystemOnTPTP comments;

clarified signature: url may change dynamically and is part of result;

clarified error;

support timeout, similar to perl LWP::UserAgent;

clarified signature;

tuned;

clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;

support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);

clarified HTTP.Content: support encoding; more realistic HTTP.Client operations;

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

more lemmas

dropped obscure FIXME

proper usage of hypotheses for zipperposition's TPTP generation

merged

tuned Mirabelle to parse option check_trivial only once

merged

merged

added stride option to Mirabelle

proper prover capabilities for zipperposition

NEWS;

merged

clarified uses of Isabelle_System.bash_process: more checks, fewer messages;

tuned signature;

more direct timing from bash_process wrapper;

tuned;

clarified signature, following Isabelle/Scala;

tuned;

clarified signature;

clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;

clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;

tuned;

clarified signature, following Isabelle/Scala;

tuned signature;

clarified signature: process_result timing from Isabelle/Scala;

NEWS

dedicated locale for preorder and abstract bdd operation

get rid of traditional predicate

proper treatment of process_result;

more accurate process_result in ML, corresponding to Process_Result in Scala;

clarified: proper trim_line for error;

unused;

clarified lines (again);

clarified modules;

more uniform Bash.process: always ask Isabelle/Scala;

more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process);

clarified compiler options;

tuned comments;

removed obsolete RC tags;

more hints;

merged

Added tag Isabelle2021 for changeset 7e2a9a8c2b85

provide naproche-755224402e36;

provide naproche-4ad61140062f;

HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.

tidied up a few ugly proofs

merged

provide naproche-6d0d76ce2f2a;

Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b

updated to flatlaf-1.0;

tuned NEWS;

tuned comments;

more robust interrupt handling as in Future.forked_results (amending 64df1e514005);

more parallelism: avoid exhaustion of standard thread pool;

more robust: resolve historic components via current tool to access current server;

tuned signature;

more parallelism;

more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;

clarified signature;

merged;

Added tag Isabelle2021-RC5 for changeset a88dbf2a020f

provide naproche-7d0947a91dd5;

more complete solutions (amending 4d36070bdbf4);

terminate faster (following dd9fc8a3036c);

more robust: accommodate output lines produced by Scala "bash_process";

updated for release;

updated to flatlaf-1.0-rc3;

more robust: allow YXML text;

inherit ISABELLE_TMP from ML process, e.g. required for $AFP/Hello_World/RunningCodeFromIsabelle.thy;

support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;

clarified modules: less redundancy;

clarified modules: allow early invocation of Scala functions;

clarified modules: allow early definition of protocol commands;

clarified links to external files, e.g. .pdf within .thy source document;

avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);

updated to flatlaf-1.0-rc2;

added lemmas

merged

updated for release;

Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb

provide naproche-20210201;

clarified messages;

more parallel;

more parallel;

contributors

hide the internal abbreviations MR and MB

optimize RBT_Impl

merged

more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);

tuned signature: more types;

clarified signature: proper order;

clarified signature: more explicit types;

tuned;

clarified signature: no symbol markup within XML attributes;

clarified signature;