Changes
#1028 (May 29, 2024, 1:45:36 PM)
#1027 (May 29, 2024, 12:18:41 PM)
#1025 (May 29, 2024, 10:45:39 AM)
#1024 (May 28, 2024, 4:42:41 PM)
#1023 (May 28, 2024, 10:00:40 AM)
#1022 (May 27, 2024, 1:45:42 PM)
- 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)
#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)
#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