more accurate rail diagram (amending de9d43c427ae);

merged

added Example theory

merged

Minor lemma tweaking

merged

merged

tuned output;

tuned comments;

clarified signature; clarified modules;

tuned;

avoid tmp files to improve robustness on Windows, where ERROR_PATH_NOT_FOUND has been seen (see also 569135d7352a);

tuned signature: more operations (following Isabelle/Scala);

more operations;

clarified signature: re-use existing Process_Result.T (NB: err_lines are de-facto program startup errors, anything else is redirected to out_lines);

tuned signature: more explicit operations;

tuned output;

misc tuning;

tuned Isabelle/ML: more uniform semicolons;

clarified signature: scalable Bash.input thanks to Bytes.T;

added time_partial_function command

A couple of theorems proved by Manuel Eberl from his AFP entry Sum_Of_Squares_Count

tuned;

tuned;

tuned signature;

proper Path.print for user output (amending 9498623b27f0);

tuned signature: more concise access to context data;

tuned English prose;

merged

tuned;

more uniform cleanup;

tuned messages;

more robust: avoid expand_path, which requires "bin/isabelle getenv"; more concise: just one ssh command; more thorough: delete etc/preferences as well;

NEWS;

enforce fresh build of HOL-Codegenerator_Test;

more platforms (untested);

update to mlton-20241230-1 using recent builds from https://sourceforge.net/projects/mlton;

update to scala-3.3.5; enforce rebuild of Isabelle/ML and Isabelle/Scala;

update for release;

Added tag Isabelle2025-RC1 for changeset ba3220909221

merged

nat_diff_split lemmas

NEWS

tuned whitespace

added lemmas ex_terminating_rtranclp_strong and ex_terminating_rtranclp

added lemma strict_partial_order_wfp_on_finite_set

proper order of operations: archive before purge;

more robust (see also 9601f5582f33);

tuned spelling;

clarified NEWS: not user-relevant;

tuned documentation;

clarified default of flatlaf.useNativeLibrary=false, for cross-platform GUI uniformity;

just one flatlaf version: native libraries are optional;

tuned;

merged

clarified name;

documentation about Build_Manager;

tuned;

use ssh host for default address;

tuned;

clarified option name;

clarified options: extra ssh connection to cluster of build_manager;

tuned output;

tuned: more standard;

merged;

more NEWS;

updated to flatlaf-3.5.4, with fallback on 2.6 for arm64-linux;

update naproche-20250201: rebuilt executables (just one copy), provide most PDFs;

tuned whitespace;

documentation about Find_Facts;

more standard: let OS pick random port by default;

clarified platforms; update to hugo-0.142.0;

tuned NEWS;

merged

more canonical formatting

add hook to insert premises in the order solver

less NEWS (see also afae60d6ff15);

switch from CVC5 to cvc5, including updates of internal tool references;

more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;

more thorough cleanup;

more options for build_release: support bundled browser_info and Find_Facts database;

more standard directory structure;

tuned output;

suppress MacOS.jar from jEdit 5.7.0, following 65fd0f032a75;

tuned GUI: attempt to improve divider mobility;

rebuild jedit component;

make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;

more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');

more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);

clarifed terminology

extracted the ^^ subtheory for modularity reasons

tuned

merged

tuned;

minor performance tuning;

tuned;

tuned names;

minor performance tuning: avoid somewhat indirect filter / add_consts;

clarified signature: more standard map_data;

misc tuning;

clarified signature with minor performance tuning: avoid Context.proof_of with its Proof_Context.init_global;

tuned names;

more explicit tests for non-PolyML SML platforms

typo

merged

more NEWS;

clarified syntax;

support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading';

more operations;

clarified signature: proper ML interface to main command, without exposing too many internals;

tuned signature: more explicit Type.raw_equiv;

more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;

move theory "HOL-Library.Adhoc_Overloading" to Pure;

discontinue odd "-build" suffix altogether (see also f51b0b54b20b, bec95e287d26, 6b45a1568637);

more frugal exports

clarified scopes

more correct SML for SML/NJ

more explicit real operations

merged

Tidied

merged

modernized and streamlined theory

provide somewhat incomplete naproche-20250125 for testing;

conservative update to stackage lts-22.15 and ghc-9.6.6;

conservative update to stack-2.15.7;

merged

merged

Tidying more old proofs

discontinue old Java 17 LTS;

update versions for release -- one behind current jedit-5.7.0;

more explicit system dependencies;

proper executable from "isabelle ocaml_opam env";

update to postgresql-42.7.5; update to sqlite-3.48.0.0; enforce rebuild of Isabelle/ML and Isabelle/Scala;

update to jdk-21.0.6; enforce rebuild of Isabelle/ML and Isabelle/Scala;

update for release;

misc tuning for release;

more NEWS;

more authors;

merged

tuned names: follow HOL Light; tuned signature: no proactive export of internal operations;

more antiquotations;

support for @{instantiate (no_beta) ...};

minor performance tuning: more fine-grained guard to skip irrelevant items;

proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);

tuned output;

minor performance tuning: omit redundant inst_cterm;

tuned signature: more operations;

misc tuning: more concise operations on prems (without change of exceptions); discontinue odd clone Drule.cprems_of (see also 991a3feaf270);

tuned: prefer Thm.prem_of, which differes wrt. exceptions that are not handled here;

tuned signature: more explicit operations;

tuned: more direct Thm.cprem_of;

misc tuning;

tuned names;

more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms; represent hyps directly, using Thm.instantiate_frees followed by freeze' to ensure that no schematic vars remain (NB: Thm.generalize ignores type information); use Thm.implies_elim / Thm.elim_implies directly, with proper exceptions instead of implicitly remaining hyps that cause trouble later; def: proper freeze after retrieval of Isabelle thm;

tuned;

misc tuning: prefer specific variants of Thm.dest_comb;

more robust: explicit check for "Trueprop";

tuned;

more robust: explicit check for "Trueprop";

clarified signature: more uniform cterm operations, without context;

tuned;

tuned;

misc tuning: more antiquotations;

clarified exceptions;

tuned names, following HOL Light sources;

more robust alignments for HOL Light Release-3.0.0;

provide num_Axiom for HOL Light Release-3.0.0; tuned proofs;

tuned proofs;

more comments; more authors;

cleanup generated bounds;

discontinue special treatment of HOL Light CONJUNCTS: this is better done in Isabelle;

clarified bundle names, in terms of the "offline" tool; option to preserve raw proofs, to allow manual experimentation with "offline" and its "maps.lst";

proper result from "offline" tool;

optional maps.lst;

tuned output: proper progress;

support tracing (with proper guard); clarified signature: more explicit type name;

more README;

allow to load additional HOL Light files, after "hol.ml";

more complete bundle;

tuned README;

proper settings;

clarified compression;

clarified patches: avoid duplication;

clarified patches;

more explicit stages, with timing messages;

avoid redundant repository clone;

move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;

original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);

tuned names;

misc cleanup and minor performance tuning;

clarified signature;

tuned: prefer existing operations;

tuned source structure;

tuned state operations;

tuned signature;

misc tuning and clarification: prefer state operations, avoid redundant ctyp_of/cterm_of;

tuned;

tuned;

tuned proofs; tuned whitespace;

merged

update to javamail-20250122;

merged

more tidying

tuned messages;

clarified: more arguments;

explicit error message when Solr database does not exist;

copy instead of symlink managed Find_Facts indexes: portable, and allows updating with local sessions;

clarified CLI arg vs. option;

clarified;

clarified find_facts URL;

clarified CLI options: web dir only in $FIND_FACTS_HOME_USER/web;

clarified settings: $FIND_FACTS_HOME_USER instead of individual directories;

clarified: Find_Facts indexes instead of Solr components;

clarified: application-specific $SOLR_DATA, e.g. $FIND_FACTS_SOLR_DATA;

merged

clarified: more operations;

tuned default nightly start: less events at 00:17:00;

use cycles in ci triggers;

varying-length calendar cycles, e.g. for ci jobs every week on a certain day/time;

clarified;

tuned whitespace;

add find_facts_index command to use within Isabelle/Scala;

clarified: add afp_root argument;

merged

introduced/overloaded power operator ^^ lists (lemmas based on AFP/Combinatorics_Words which defines ^@)

systematic checks for bit operations and more rules on symbolic terms

explicitly report dependencies on missing code equations

simplified old proofs

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;

clarified GUI: more auto_hovering_button instances;

more robust: prefer official BasicSplitPaneUI operations;

clarified split_pane layout: close on first display, open on first search;

more operations, specifically for FlatLaf;

added documentation for new Sledehammer option "cache_dir"

updated affiliation in Sledgehammer documentation

merged

added option "cache_dir" to Sledgehammer

more simp rules on word conversions

spelling;

update to xz-java-1.10;

update to zstd-jni-1.5.6-8;

update to sqlite-3.47.1.0; enforce rebuild of Isabelle/Scala and Isabelle/ML;

updated to postgresql-42.7.4; enforce rebuild of Isabelle/Scala and Isabelle/ML;

update to llncs-2.25;

update to jsoup-1.18.3; enforce rebuild of Isabelle/Scala;

clarified signature;

tuned proofs; tuned whitespace;

avoid duplicate markup, notably from "CONST c";

clarified pretty_entity for syntax consts without mixfix annotation (see also 43c4817375bf and d622145603ee);

tuned;

clarified signature (see also 2157039256d3);

more syntax bundles, e.g. to explore terms without notation;

commands 'syntax_types' and 'syntax_consts' now work in a local theory context;

tuned names;

tuned signature: avoid shadowing;

syntax translations now work in a local theory context;

clarified signature;

clarified signature and modules;

minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;

tuned whitespace;

tuned proofs;

tuned proofs;

clarified class/locale reasoning: avoid side-stepping constraints;

clarified default_sort: "cpo" for bootstrap, "domain" for main HOLCF;

clarified specification context;

activate e-3.1 as proposed by Martin Desharnais; enforce rebuild of Isabelle/ML;

more robust: avoid spurious crash of text_area.getText() in Active_Area.update();

proper bundle binomial_syntax; NB: precedence of "choose" changes silently from 65 to 64 in 200107cdd3ac, but old 65 was still seen in the wild;

build component for cvc5-1.2.0;

tuned whitespace;

clarified default_sort;

fewer theories;

fewer theories;

fewer theories (in contrast to 05ca920cd94b);

more accurate markup for "CONST c";

tuned markup;

proper LaTeX setup (amending 41b387d47739);

more LaTeX markup for printed entities;

tuned;

tuned;

more HTML markup (without rendering);

more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;

tuned: more robust wrt. changes the Markup space;

tuned: prefer explicit names of inferred types;

more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c);

clarified signature;

tuned;

clarified signature;

clarified term positions and markup: syntax = true means this is via concrete syntax; clarified text color rendering;

tuned signature: more operations;

tuned;

clarified signature: more explicit operations;

tuned;

tuned whitespace;

clarified signature and caching;

clarified GUI: prefer user documents, which are typically without chapter;

tuned;

obsolete;

tuned signature;

merged

NEWS;

clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;

tuned signature;

clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");

prefer Term.variant_bounds: bounds vs. frees, no attempt at consts;

more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;

tuned signature;

clarified modules;

more accurate extern_const: avoid clash with frees;

more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;

clarified signature: uniform context;

clarified signature: uniform context;

proper context for extern operation: observe local options; more uniform global_ctxt for pretty printing;

proper context for extern/check operation: observe local options like names_unique;

tuned;

tuned signature: more operations;

added Halting problem theory

merged

added parallel_group_size option to Mirabelle

adapted bash files to use cartouches

tuned

clarified names context: proper context, without consts;

clarified names context: proper context, without consts;

tuned;

tuned;

clarified signature: more operations;

merged

clarified signature;

tuned names/scopes;

tuned signature: more operations;

eliminate historic clone (see also 550e36c6a2d1);

tuned signature: more operations;

clarified 'unbundle' polarity, according to algebraic group laws;

tuned signature: more operations;

tuned: more direct use of Name.context operations;

tuned;

misc tuning and clarification: more direct use of Name.context operations;

tuned signature: more operations;

tuned: more direct use of Name.context operations;

clarified signature: shorten common cases;

tuned: more standard Name.build_context, although that is a bit longer;

clarified signature: more uniform;

omit redundant combinators (amending 7456a64bc4f6);

tuned signature;

fixed bugs found by Stepan Holub

merged

added lemmas

merged

more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);

clarified signature and object initialization;

clarified default: avoid copies;

suppress odd icons for documents and folders;

support for modified tree cell renderer;

clarified signature: avoid implicit functionality;

re-use Output_Area;

re-use Output_Area;

re-use Output_Area;

re-use Output_Area with search results;

re-use Output_Area with search results;

more thorough init;

clarified signature: prefer defaults for Output_Dockable (and its variants);

unused;

tuned output: formatting is pointless for proportional font;

clarified Tree_View.init_model: more uniform;

more robust update;

handle tree selection;

Output_Dockable: show search results as tree view;

clarified modules;

clarified signature;

clarified signature;

clarified signature and modules: without GUI change yet;

more operations, to support search within output panel;

tuned;

Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

Patch by Stepan Holub, plus tweaks

patch to vector_matrix_mult by Alexander Pach

try0: cleaned up output;

try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;

avoid informatik.tu-muenchen.de domain: soon to be discontinued;

renamed Discrete -> Discrete_Functions to avoid name clashes; new function names floor_log/sqrt to avoid long Discrete_Functions.log/sqrt

Use Var to maintain the difference between function and locale parameters

tuned

tuned proofs;

tuned proofs;

minor performance tuning: avoided repeated metric initialization;

tuned signature: more operations;

clarified signature;

more NEWS;

tuned proofs;

merged

enforce rebuild of Isabelle/ML and Isabelle/Scala;

update to jedit-20241115 (see also ecd62f7b3644 and d92d754b5dd9);

more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);

tuned comments;

clarified key events: cancel output selection, before input selection;

proper focus to support subsequent copy-paste via keyboard;

more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";

removed obsolete option: jEdit 5.7.0 can be built with default jdk;

more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);

less ambitious selection;

mv Discrete to Discrete_Cpo to avoid theory name clashes

disable 2d9b6e32632d for now: unknown problems on macOS;

clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);

more careful isConsumed() / consume() for key and mouse events;

merged

added field input_eqns to record the list of equations (the specification) given to the function command.

merged

more NEWS;

tuned proofs;

more ambitious mouse handler: double-click selects highlight_area;

more accurate mouse handler: only for single clicks, consume accepted event;

more ambitious scrolling: retain original scroll position if possible;

more ambitious scrolling: retain bottom position after output;

performance tuning: cache for Rich_Text.format, notably for incremental tracing;

clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;

omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;

tuned;

minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);

clarified signature and modules; more basic Rich_Text.formatted_lines, assuming that elements are properly separated according to Rich_Text.format;

performance tuning for macOS (after update of "jedit" component): old OpenGL works better for text rendering;

performance tuning: more incremental update of buffer content;

obsolete;

clarified: more uniform results;

clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();

minor performance tuning: avoid concatenation of existing string material;

clarified signature and data storage: incremental lazy values;

tuned comments;

clarified signature;

clarified modules;

clarified margin operations (again, reverting 4794576828df);

clarified modules;

more reactive interrupts (via Future.cancel);

Document.Snapshot: support for multiple snippet_commands; clarified Command.rich_text: prefer explicit id, e.g. from message serial; clarified Pretty_Text_Area.update: Protocol_Message.provide_serial; clarified Pretty_Text_Area.format_rich_texts, with separate formatting of messages;

more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;

clarified signature: include standard margin in object equality;

performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);

The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2

merged

merged

clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);

clarified signature;

tuned GUI: avoid wasting space with proportional fonts;

clarified signature;

more accurate pretty_margin for proportional fonts;

clarified signature: more uniform;

tuned: fewer warnings in IntelliJ IDEA;

tuned signature;

tuned signature;

clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;

more accurate message boundaries;

tuned whitespace;

clarified signature: more robust type XML.Elem;

clarified signature;

clarified signature;

clarified output representation: postpone Pretty.separate;

tuned;

tuned: fewer warnings in IntelliJ IDEA;

clarified signature: more accurate types;

tuned signature: more standard names;

more uniform pretty_text_area.zoom via its zoom_component;

tuned signature;

tuned signature: more standard names;

tuned;

clarified signature;

clarified signature;

tuned;

revert 1206400b9b48: proper Node.unapply for Node.apply(null);

tuned signature;

clarified signature;