sledgehammer pretty-printing: merge x(1) x(2) to x(1,2) — nipkow / hgweb
tuned; — wenzelm / hgweb
tuned spelling; — wenzelm / hgweb
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs"); — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
more general dirs for Sync.sync; — wenzelm / hgweb
tuned whitespace (amending beb4ee344c22); — wenzelm / hgweb
clarified signature (see also be0ab4b94c62 and c41791ad75c3); — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned names; — wenzelm / hgweb
proper SSH.System operation; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
more uniform/robust detect_repository/is_repository: actually check hg root; — wenzelm / hgweb
more uniform local/remote operations; — wenzelm / hgweb

#1021 (May 24, 2024, 5:03:09 PM)

pretty-printing: merge multiple indexed facts of the same name — nipkow / hgweb
disable Isabelle/Naproche after release; — wenzelm / hgweb
post-release updates; — wenzelm / hgweb
merged — wenzelm / hgweb
Added tag Isabelle2024 for changeset 29f2b8ff84f3 — wenzelm / hgweb
proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f); — wenzelm / hgweb
provide scala-3.4.2, but do not activate it: scala-3.3.x is LTS version; — wenzelm / hgweb
update to naproche-20240519; — wenzelm / hgweb
proper formatting; — wenzelm / hgweb
more documentation on "isabelle build -H" and underlying system registry tables "host" and "cluster"; — wenzelm / hgweb
More binomial material — paulson <lp15@cam.ac.uk> / hgweb
syntax of gchoose now the same as choose — paulson <lp15@cam.ac.uk> / hgweb

#1020 (May 6, 2024, 3:42:23 PM)

Some new simprules – and patches for proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
tuned proofs;
tuned whitespace; — wenzelm / hgweb
merged, resoving conflicts in src/HOL/Nominal/Nominal.thy; — wenzelm / hgweb
Added tag Isabelle2024-RC3 for changeset 007e6af8a020 — wenzelm / hgweb
more documentation on "System registry via TOML"; — wenzelm / hgweb
update to naproche-20240502: proper platform_path for NAPROCHE_FORMALIZATIONS to make it work on Windows; — wenzelm / hgweb
provide 3.1 for testing (inactive); — wenzelm / hgweb
build e-3.1, without patch; — wenzelm / hgweb
disable Isabelle/Naproche for now: does not quite work on Windows; — wenzelm / hgweb
update and activate naproche component for release; — wenzelm / hgweb
changed URL to SystemOnTPTP at Geoff's request — desharna / hgweb
tuned spelling; — wenzelm / hgweb
build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state; — wenzelm / hgweb
proper directory permissions to make "rm" work, notably for cygwin/etc/pki/ca-trust/extracted/pem/directory-hash; — wenzelm / hgweb
support more Ubuntu versions; — wenzelm / hgweb
updated for release; — wenzelm / hgweb
more robust: avoid spurious ConcurrentModificationException; — wenzelm / hgweb
update to e-3.0.03-1, with proper support for trivial statements; — wenzelm / hgweb
more robust; — wenzelm / hgweb
minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements; — wenzelm / hgweb
backed out changeset 601ff5c7cad5: not relevant for Isabelle2024; — wenzelm / hgweb
clone of 0c51e0a6bc37; — wenzelm / hgweb
merged — paulson / hgweb
update Windows test machines; — wenzelm / hgweb
A little more tidying in Nominal — paulson <lp15@cam.ac.uk> / hgweb
More tidying of proofs — paulson <lp15@cam.ac.uk> / hgweb
Another Nominal example — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
update Windows build host; — wenzelm / hgweb
proper command-line; — wenzelm / hgweb
Tidying up another Nominal example (SOS) — paulson <lp15@cam.ac.uk> / hgweb
Tidying up another of the nominal examples — paulson <lp15@cam.ac.uk> / hgweb
More tidying of Nominal proofs — paulson <lp15@cam.ac.uk> / hgweb
Tidied up another messy theory — paulson <lp15@cam.ac.uk> / hgweb
More proof tidying for Nominal — paulson <lp15@cam.ac.uk> / hgweb
Tidying up more messy proofs — paulson <lp15@cam.ac.uk> / hgweb
Starting to tidy HOL-Nominal-Examples — paulson <lp15@cam.ac.uk> / hgweb
sketch & explore: recover from duplicate fixed variables in Isar proofs — Simon Wimmer <wimmers@in.tum.de> / hgweb
back to post-release mode -- after fork point; — wenzelm / hgweb
merged — wenzelm / hgweb
Added tag Isabelle2024-RC2 for changeset ef2134570abb — wenzelm / hgweb
Acknowledgement of Ata Keskin for his Martingales material — paulson <lp15@cam.ac.uk> / hgweb
merged — wenzelm / hgweb
update to jdk-21.0.3;
enforce rebuild of Isabelle/ML and Isabelle/Scala; — wenzelm / hgweb
merged — paulson / hgweb
clarified signature; — wenzelm / hgweb
make adhoc_overloading respect type constraints — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
merged — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
minor performance tuning: avoid redundant server access; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules and options (from store); — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4); — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
tuned; — wenzelm / hgweb
back to static numa_nodes (reverting part of c2c59de57df9); — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
canonical time function for List.nth — Manuel Eberl <eberlm@in.tum.de> / hgweb
Tidied up horrible archaic proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces); — Fabian Huch <huch@in.tum.de> / hgweb
Streamlining of many more archaic proofs — paulson <lp15@cam.ac.uk> / hgweb
More tidying of old proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
Add subgoals variant of 'sketch' command — Simon Wimmer <wimmers@in.tum.de> / hgweb
More tidying and removal of "apply" — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
prefer canonical theorem name for fact collection declarations — haftmann / hgweb
Tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
tuned; — Fabian Huch <huch@in.tum.de> / hgweb
Tidying ugly proofs — paulson <lp15@cam.ac.uk> / hgweb

#1019 (Apr 11, 2024, 2:15:11 PM)

tweaked time functions for median-of-medians selection in HOL-Data_Structures — Manuel Eberl <manuel@pruvisto.org> / hgweb
merged — wenzelm / hgweb
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta; — wenzelm / hgweb
Tiny tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb
A bit of new material about type class "infinite", from Eval_FO — paulson <lp15@cam.ac.uk> / hgweb
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax; — wenzelm / hgweb
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); — wenzelm / hgweb
adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested; — wenzelm / hgweb
Add entry on Sketch_and_Explore to CONTRIBUTORS — Simon Wimmer <wimmers@in.tum.de> / hgweb
moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); — wenzelm / hgweb
tuned signature; — wenzelm / hgweb

#1018 (Apr 4, 2024, 3:30:29 PM)

moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
documented new syntax for fBall and fBex — desharna / hgweb
updated for release; — wenzelm / hgweb
Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 — wenzelm / hgweb
misc tuning for release; — wenzelm / hgweb
update for release; — wenzelm / hgweb
merged — wenzelm / hgweb
update to stack-2.15.5, stackage-lts-22.15; — wenzelm / hgweb
clarified names: discontinue odd convention from 3 decades ago; — wenzelm / hgweb
further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations; — wenzelm / hgweb
added documentation for meromorphicity etc. in HOL-Complex_Analysis — Manuel Eberl <manuel@pruvisto.org> / hgweb
merged — desharna / hgweb
remove transitional (dummy) component list for Go — Lars Hupel <lars@hupel.info> / hgweb

#1017 (Apr 2, 2024, 8:36:08 AM)

merged — desharna / hgweb
clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code; — wenzelm / hgweb
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
NB: Simplifier.set_trace_ops overrides Pure setup for Simplifier_Trace panel, but that is hardly every used in practice; — wenzelm / hgweb
provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version; — wenzelm / hgweb
clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow"; — wenzelm / hgweb
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
update NEWS; — Fabian Huch <huch@in.tum.de> / hgweb
moved web_app module from AFP (e.g., for building web services for the distributed build); — Fabian Huch <huch@in.tum.de> / hgweb
added special syntax for FSet.Ball and FSet.Bex — desharna / hgweb
tuned proof — desharna / hgweb
tuned proofs of Equiv_Relations.equiv — desharna / hgweb

#1016 (Mar 29, 2024, 7:30:12 PM)

moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
tuned; — Fabian Huch <huch@in.tum.de> / hgweb
removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML); — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified modules: more official Sessions.notable_groups; — wenzelm / hgweb
tuned — nipkow / hgweb
merged — paulson / hgweb
An assortment of new material, mostly due to Manuel — paulson <lp15@cam.ac.uk> / hgweb

#1015 (Mar 28, 2024, 3:24:23 PM)

test — wenzelm / hgweb
rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;
provide official etc/platforms.props, to retain platform directories after Components.Directory.clean() -- e.g. for SSH upload; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb

#1014 (Mar 28, 2024, 1:39:38 PM)

test — wenzelm / hgweb

#1013 (Mar 28, 2024, 8:33:11 AM)

tuned proofs of Equiv_Relations.equiv — desharna / hgweb
merged — desharna / hgweb
proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests; — wenzelm / hgweb
proper "isabelle go_setup" for Jenkins; — wenzelm / hgweb
added lemma wfp_on_image and author name to theory — desharna / hgweb

#1012 (Mar 27, 2024, 10:09:08 PM)

proper "isabelle go_setup" for Jenkins; — wenzelm / hgweb
dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24); — wenzelm / hgweb
tuned message; — wenzelm / hgweb
merged — wenzelm / hgweb
merged — nipkow / hgweb
updated time functions for Array_Braun — nipkow / hgweb
merged — paulson / hgweb
New material and a bit of refactoring — paulson <lp15@cam.ac.uk> / hgweb
tuned NEWS; — wenzelm / hgweb
support for "all" platforms; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and 37f852399a32); — wenzelm / hgweb
tuned; — wenzelm / hgweb
more robust Markdown; — wenzelm / hgweb
misc tuning;
more text; — wenzelm / hgweb
run "isabelle components_build -u"; — wenzelm / hgweb
remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup"; — wenzelm / hgweb
tuned order; — wenzelm / hgweb
more Setup_Tool services; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
proper SSH operations; — wenzelm / hgweb
tuned signature: more permissive; — wenzelm / hgweb
clarified signature: explicit variable is easier to find in source; — wenzelm / hgweb
proper services for Setup_Tool --- avoid hardwired stuff; — wenzelm / hgweb

#1011 (Mar 27, 2024, 11:51:11 AM)

added lemma wfp_on_image and author name to theory — desharna / hgweb
merged — desharna / hgweb
more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML); — wenzelm / hgweb
more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51); — wenzelm / hgweb
misc tuning for release; — wenzelm / hgweb
merged; — wenzelm / hgweb
NEWS for "isabelle go_setup"; — wenzelm / hgweb
proper platform_path for Windows; — wenzelm / hgweb
misc tuning, following go_setup; — wenzelm / hgweb
dynamic setup of Go component, similar to Dotnet; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
clarified signature: more operations; — wenzelm / hgweb
clarified signature: explicit type Platform.Info with derived operations; — wenzelm / hgweb
less ambitious parallelism: avoid exhaustion of memory (64GB total); — wenzelm / hgweb
provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup"; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
update to bash_process-20240326; — wenzelm / hgweb
build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all platform directories (e.g. for SSH upload); — wenzelm / hgweb
clarified meaning of platform.props: update on default; — wenzelm / hgweb
allow raw input in HTML (e.g., for web applications); — Fabian Huch <huch@in.tum.de> / hgweb

#1010 (Mar 26, 2024, 2:37:33 PM)

renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal — desharna / hgweb

#1009 (Mar 26, 2024, 9:33:11 AM)

added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on — desharna / hgweb
merged — desharna / hgweb
obsolete: base-line is macOS 11; — wenzelm / hgweb
more robust: always assume x86_64 (or its emulation on ARM); — wenzelm / hgweb
MLton lacks arm64-linux (see also 84f2d481d6d7); — wenzelm / hgweb
more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for AFP on lrzcloud2; — wenzelm / hgweb
update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — wenzelm / hgweb
misc updates, tuning and clarification; — wenzelm / hgweb
reformat source in jEdit (wrap margin 78); — wenzelm / hgweb
more accurate Markdown formatting, both for VSCode and Phabricator; — wenzelm / hgweb
just one README.md; — wenzelm / hgweb