merged

merged

A variety of tweaks

avoid legacy warnings in "test_code check in OCaml";

proper condition for strict "test_code check in OCaml" and "test_code check in GHC";

more NEWS;

merged

misc tuning;

tuned;

tuned;

clarified pattern matching;

misc tuning;

misc tuning and clarification;

tuned;

clarified exceptions and messages: use "error" only for user-errors, not system failures;

minor performance tuning: more elementary operations;

minor performance tuning;

clarified inst_type: more direct Thm.instantiate_frees;

more direct Thm.free: avoid re-certification;

clarified signature: more explicit types;

tuned names;

tuned names;

tuned signature;

tuned;

tuned signature;

clarified signature: more standard Isabelle/ML;

clarified signature;

more robust import_file path: proper master_directory; support for compressed proofs.zst (e.g. via "zstd -8");

tuned signature: more operations;

unused;

tuned signature, following Isabelle/Scala;

clarified signature, following Isabelle/Scala;

clarified pattern via antiquotations;

misc tuning and clarification;

tuned;

clarified make_type: proper make_name;

tuned;

tuned;

clarified signature: more standard Isabelle/ML;

reproducible construction of HOL Light export bundle;

tuned messages;

more robust options; more robust lines;

clarified signature: more explicit operations;

tuned;

tuned: prefer inlined thms;

tuned proofs;

proper GUI.Style_HTML.make_text, e.g. for term "x < y";

clarified signature: more explicit operations;

provide less ambitious "isabelle ocaml_setup_base", notably for platforms without gmp-dev;

clarified signature: more explicit operations;

update to ocaml-base-compiler.4.14.1, which coincides with ocaml on Ubuntu 24.04;

isabelle_id: report sync id, if available;

clarified: sync_id operation, similar to archive_id;

build schedule: limit history length;

tuned whitespace;

restrict check to PolyML

merged

More tidying of old proofs

dropped redundant material (left-over from 5e3dd01a9eb2)

explicit check for (experimentally determined) border value

theory to rewrite arithmetic operations to bit shifts

merge

Compact notation for Suc numerals.

store the {l,g}fp-definition and the monotonicity theorem for inductive predicates (by Jan van Brügge)

make the definition of BNF bounds more easily accessible (by Jan van Brügge)

avoid theorem name clash (by Jan van Brügge)

introduce fewer constants in copy_bnf/lift_bnf (by Jan van Brügge)

Some work on an ancient theory file. And a weird failure in Float.thy

simplified old proofs

polished messy proofs

moved lemmas to book

merged

tuned messages: more verbosity;

more explicit default_port;

tuned messages;

tuned;

proper initialization of settings: avoid accidental intrusion from parent process environment;

clarified solr_data directory, provided via settings;

explicit settings FIND_FACTS_WEB and option -w, outside of source (immutable) directory;

tuned message;

implicit session build, similar to "isabelle export";

tuned message;

proper Console_Progress as for other command-line tools;

tuned messages: more formal;

clarified signature: progress is usually optional;

clarified names: "peek" usually refers to evolving mutable state;

more to check;

tuned: avoid "open" in ML and "import _" in Scala;

tuned messages;

tuned headers;

more to check;

clarified names;

clarified signature and modules;

tuned;

avoid conflict with slf4j from sqlite (see also dcddfe4f43a3), notably this message on "isabelle find_facts": SLF4J(W): Class path contains multiple SLF4J providers. SLF4J(W): Found provider [org.slf4j.nop.NOPServiceProvider@1576514a] SLF4J(W): Found provider [org.apache.logging.slf4j.SLF4JServiceProvider@6a84d4e3] SLF4J(W): See https://www.slf4j.org/codes.html#multiple_bindings for an explanation. SLF4J(I): Actual provider is of type [org.slf4j.nop.NOPServiceProvider@1576514a]

misc tuning;

tuned: fewer warnings in IntelliJ IDEA;

tuned headers;

tuned headers;

more NEWS + CONTRIBUTORS;

tuned comments;

tool wrappers with specific java options, notably classpath "$SOLR_JARS";

clarified options;

proper component src/Tools/Find_Facts; clarified directory structure;

components for find_facts;

suppress duplicate slf4j-api --- already provided by sqlite;

clarified solr settings; proper version;

proper platform.exe;

activate admin tools; clarified elm settings;

original sources of find-facts 271b5af0c4c8;

Simplified a lot of messy proofs

compatibility with Scala 3

more correct code generation for string literals

made lemma visible

fixed a typo

Correction to pretty printing for set intervals, allowing a line break if necessary for a large expression

tuned documentation and order of instantiated facts

merged

update cygwin near 3.5.5-1, see also https://cygwin.com/pipermail/cygwin-announce/2024-December/012023.html

direct symbolic implementations of and, or, xor on integer

corrected

merged

remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);

rebuild cvc5 component (still inactive); more robust workaround on all platforms, avoid crash of "sledgehammer [cvc5]" seen on x86_64-linux after line 75 of "$AFP/thys/Boolos_Curious_Inference_Automated/Boolos_Curious_Inference_Automated.thy";

tuned spacing

merged

tuned Sledgehammer caching

Rename "suggest_of" to "instantiate"

merged

added lemmas

discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);

more markup, notaly for LaTeX output: treat record fields as quasi-consts;

tuned: more direct string comparison (see also 6e25f82056ad, where the explanation was actually wrong: about fast_string_ord instead of string_ord);

update release name;

Added tag Isabelle2025-RC0 for changeset bcb793b951c0

proper NEWS section;

proper latin "A" instead of greek "Alpha";

update to current jcef-1.0.61;

recovered "isabelle component_jcef" from bf537a75e872, adapted to 9fe5d8c70352 and 2a99fcb283ee;

tuned proofs;

tuned proofs;

more robust afp_repository, with regular hgweb URLs;

more documentation;

merged

tuned;

tuned (NB: string_ord is required here for its precedence on length);

more robust: ensure that Nginx is not superseded by implicit Apache dependencies (Ubuntu 24.04);

tuned NEWS;

drop obsolete URLs;

updated Ubuntu versions;

more robust defaults, notably for Ubuntu 24.04;

delegate computation to integer thoroughly

merged

more robust: ensure that /run/sshd is present, which is required for ExecStartPre phase;

some support for Ubuntu 24.04;

tuned names: more uniform;

update NEWS / documentation / descriptions for Phorge (formerly Phabricator);

unused;

follow Phorge 2024 week 35;

separate theory for tests checking bit operations

optionally use shift operations on target numerals for efficient execution

some bit operations on target numerals

rebuild E 3.1 on Windows/Cygwin, with patch for proper interrupts;

misc tuning and clarification: more explicit types; proper normal form for repeated text entries;

misc tuning and updates for release;

tuned NEWS;

provide component cvc5-1.2.0, including arm64-linux; workaround for ARM64 platform, avoid odd crash of "sledgehammer [cvc5, mepo, slices = 4]" before line 318 of "$AFP/thys/Given_Clause_Loops/DISCOUNT_Loop.thy";

refined syntax for code_reserved

explicit error message for non-existing code target

revert changeset 2f98e3c4592c: avoid conflict with low-level \<^latex> markup;

merged

more robust LaTeX setup, notably for Ubuntu 24.04;

tuned;

proper treatment of markup within line indentation, notably for Latex.output_ops;

misc tuning and clarification: more explicit types;

more accurate indentation: retain (before: Double) until it is materialized as blanks;

misc tuning: more uniform;

clarified internal data representation, following push/pop model of Scala version;

tuned names;

more accurate formatting of open_block: markup only, without affecting layout (e.g. via force_next); tuned signature;

tuned: more uniform;

proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);

tuned;

unused;

tuned signature;

tuned: more uniform;

tuned: more uniform;

clarified data representation: less redundancy;

tuned;

minor performance tuning;

clarified signature: more direct indent_markup; minor performance tuning: bypass "ind" buffer when unused;

more LaTeX markup;

Backed out changeset 0ca0a47235e5 (produced Code check failed for Haskell?)

tuned

merged

merged

merged

tuned slow proof

merged

proper bullet symbols for GUI text -- in contrast to Isabelle \<bullet> 0x002219;

tuned: more direct GUI painting via HTML;

tuned generated output: more standard operations;

tuned GUI output: more uniform;

minor performance tuning;

tuned generated output: more standard operations;

clarified signature: more operations;

more accurate treatment of plain text (amending eede0cf38a63);

clarified signature: more operations;

clarified signature;

tuned, following theories_status.scala;

tuned imports;

tuned GUI output;

clarified signature: ensure uniform style;

tuned GUI output;

clarified signature;

tuned;

clarified signature;

drop redundant space in HTML (see also 18a720984855);

clarified signature;

more robust: proper HTML.output;

tuned signature;

tuned: fewer warnings in IntelliJ IDEA;

clarified output;

clarified signature;

more GUI styles;

clarified signature;

tuned signature;

tuned: fewer warnings in IntelliJ IDEA;

tuned: fewer warnings in IntelliJ IDEA;

tuned proofs;

some bit operations on target numerals

explicit tests for target-language bit operations

avoid default simp rule which would produce strange recursive unfolding in presence of bit_eq_iff

update to xz-java-1.10 for further testing (see also fe7238c01809); enforce fresh build of Isabelle/Scala and Isabelle/ML;

more default simp rules

back to xz-java-1.9, to see if this improves build_manager stability; enforce rebuild of Isabelle/ML and Isabelle/Scala, in a robust manner using random UUID;

merged

revered the hiding of the standard nat theorems

minor performance tuning; directly try to read file instead of first checking its existence

merged

minor performance tuning; avoid constructing path if unused and double construction

merged

more markup: for diagnostic purposes of ambig_msgs;

more uniform Markup.notation vs. Markup.expression;

tuned output: suppress vacuous nodes from 07ad0b407d38;

clarified LaTeX presentation: more specific keywords;

clarified literal data;

merged

tuned ATP caching in Sledgehammer to consider the command line

tuned function lines_of_atp_problem to have header lines as proper list elements

tuned tests for existing directories in Sledgehammer

merged

tuned GUI: more informative search_title;

clarified induct rules: proper case_names; tuned proofs;

tuned proofs;

tuned GUI: trim text as in org.gjt.sp.jedit.search.HyperSearchResult;