NEWS

added Mirabelle option "-y" for dry run

tuned garbage optimization

added cpu time (in ms) to Mirabelle run_action output

added Mirabelle option -r to randomize the goals before selection

A new lemma about inverse image

proper treatment of $let variables in symbol table in Sledgehammer

removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer

merged

split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"

proper name mangling of "undefined" constants in Sledgehammer

earlier availability of lifting

more correct transfer

merged

proper abstraction of function variables when instantiating induction rules in Sledgehammer

added lemma asympD

added lemma

Some lemmas about continuous functions with integral zero

merged

added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp

removed $ite from E 2.6 in THF format

New and simplified theorems

merged

prefixed all mirabelle_sledgehammer output lines with sledgehammer output

added lemma

Tiny additions inspired by Roth development

allow general command transactions with presentation;

more operations;

clarified signature;

tuned signature;

support Gradle as alternative to Maven (again);

tuned mirabelle command-line help message

updated Mirabelle documentation

proper documentation for induction_rules Sledgehammer option

NEWS

merged

used TH1 for Leo-III in sledgehammer

tuned run_sledgehammer and called it directly from Mirabelle

exported Sledgehammer.launch_prover and use it in Mirabelle

proper filtering inf induction rules in Mirabelle

added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle

tuned ATP to use is_widely_irrelevant_const

added support for initialization messages to Mirabelle

tuned comment

support for JSON:API;

support for Flarum server;

tuned whitespace;

tuned imports;

tuned comments;

clarified author names;

clarified author names;

merged

more accurate names; complete coverage of mail addresses;

more standard author_info;

clarified author info and cluster nodes;

more data integrity: name vs. address;

clarified signature: more operations;

clarified signature;

tuned;

more data integrity: name vs. address;

tuned comments;

merged

tuned ATP to use fold_index

tuned sledgehammer to use map_index

merged

more data integrity: name vs. address;

misc tuning and clarification;

clarified name;

more mailing list content;

more mailing list content;

updated links;

added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff;

tuned ATP to use map_index

removed obsolete RC tags;

proper path;

merged, resolving conflict in src/Doc/Implementation/Logic.thy;

Added tag Isabelle2021-1 for changeset c2a2be496f35

tuned;

proper ML types (amending 1aa92bc4d356);

proper types for Scala.Fun instances (amending 1aa92bc4d356);

proper syntax category;

provide component naproche-20211211;

merged

more Mailman archives;

more Mailman content;

clarified signature;

tuned metis to use map_index

merged

fixed HOL-TPTP

tuned vars_of_iterm

fixed TPTP generation of multi-arity expressions

proper handling of Hilbert choice in TFX logics

proper tptp_builtins

reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle

proper proxy for Hilbert choice in TPTP output

proper polymorphism for TH1 format in Sledgehammer

refactored $ite and $let configuration and added dummy_thf_reduced prover

tuned TPTP file names generated by Sledgehammer

tuned SMT-Lib file names generated by Mirabelle

added support for higher-order SMT proof search in Sledgehammer

separated FOOL from $ite/$let in TPTP output

missing latex font

Rewrite: added links to docu, made more prominent

discontinued old-style {* verbatim *} tokens;

tuned proof;

isabelle update_cartouches;

more symbolic latex_output via XML (using YXML within text);

tuned signature: remove unused;

prefer symbolic Latex.environment (typeset in Isabelle/Scala);

tuned signature;

clarified corner cases of syntax;

clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);

a slightly simpler proof

provide component naproche-2d99afe5c349;

merged

Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2

more documentation about Type/Const antiquotations;

more documentation about document build options;

address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c);

tuned --- fewer IDE warnings;

more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing;

added definitions multp{DM,HO} and corresponding lemmas

added wfP_less to wellorder and wfP_less_multiset

restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3

merged

added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset

redefined less_multiset to be based on multp

added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp

added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max

added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp

added lemma wfP_multp

added lemma mono_multp

added Multiset.multp as predicate equivalent of Multiset.mult

address problems with launch4j and jdk-17 (see also 41d009462d3c);

more robust build on midrange hardware;

clarified tests: omit somewhat pointless (unstable) results;

proper fields for gnuplot (amending b614e3e4146a);

tuned output;

tuned;

merged

more robust build on midrange hardware (despite 67d6f1708ea4);

Added tag Isabelle2021-1-RC4 for changeset 2336356d4180

updated to polyml-5.9;

NEWS on "isabelle mirabelle";

tuned;

clarified default for kodkod_scala; NEWS for proper release;

maintain option kodkod_scala within theory context, to allow local modification;

NEWS for proper release;

updated to flatlaf-1.6.4;

avoid broken links: auxiliary files are not yet supported;

option document_comment_latex supports e.g. Dagstuhl LIPIcs;

more explicit type Latex.Tags; generate isabelletags.sty from Isabelle/Scala, including comment.sty setup;

more uniform treatment of optional_argument for Latex elements; discontinued somewhat pointless element position in Isabelle/Scala: semantic add-ons are better provided in Isabelle/ML; clarified signature of class Latex: overridable unknown_elem allows to extend the markup language;

removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;

example: alternative document headings, based on more general document output markup;

more general document output: enclosing markup is defined in user-space;

clarified modules (see c299abcf7081);

output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;

clarified modules;

tuned signature: more explicit types for presentation;

more robust support for Windows line-endings;

source positions for document markup commands, e.g. to retrieve PIDE markup in presentation;

more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;

clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true";

more symbolic latex_output via XML (using YXML within text);

proper enclose_name (amending e77c5bfca9aa);

Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.;

more symbolic latex_output via XML;

clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);

tuned;

tuned;

updated to verit-2021.06.2-rmx;

clarified HTML_Context.theory_exports: prefer value-oriented parallelism;

generate problems with correct logic for veriT

more parallelism, at the cost of potential duplicates of make_thy;

afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);

more interrupts;

present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826; eliminated implicit state: these theories are globally unique;

tuned;

clarified modules;

tuned (see also e0d1d9203275);

clarified signature;

tuned;

spelling;

added asymp_{less,greater} to preorder and moved mult1_lessE out

renamed multp_code_iff and multeqp_code_iff

simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0

renamed Multiset.multp and Multiset.multeqp

added lemmas

merged

tuned;

removed redundant test (see also 86fac52c2795, a9fea3f11cc0);

just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);

proper version;

back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834);

less ambitious parallelism: more direct read/write saves overall heap space and GC time;

slightly faster XML output: avoid too much regrowing of StringBuilder;

updated NEWS: arm64-linux support is almost complete;

update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;

more material for HOL-Analysis.Infinite_Sum

more symbolic latex_output via XML;

clarified signature;

updated to polyml-5.9-610a153b941d -- close to final;

tuned signature (again): latex_output is likely to depend on context;

more symbolic latex output; discontinued Latex.output_text, which is in conflict with symbolic output;

tuned signature;

symbolic latex_output via XML, interpreted in Isabelle/Scala;

tuned signature;

clarified signature;

clarified signature;

clarified signature: more privacy;

tuned output --- less redundancy;

tuned whitespace;

clarified signature: Latex.Output as parameter to Document_Build.Engine; tuned;

proper detection of ARM platform variants;

back to post-release mode;

updated for release;

Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5

merged

updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default);

clarified HTML_Context: more explicit directory structure;

tuned comments;

tuned;

clarified signature;

clarified properties: avoid empty entry;

tuned signature;

merged

tuned (thanks to J. Villadsen)

added padding to Mirabelle's output

merged

tuned generation of TPTP with $ite/$let in higher-order logics

tuned generation of TPTP with $ite in function position

tuned TPTP generation of If helper facts

merged

clarified signature: prefer static operations;

clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;

more robust;

tuned signature;

clarified signature: more explicit class Entity_Context with private state + operations;

more hyperlinks, notably internal fact references;