isabelle: Graph

proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f); Isabelle2024
14 months ago, by wenzelm
provide scala-3.4.2, but do not activate it: scala-3.3.x is LTS version;
14 months ago, by wenzelm
update to naproche-20240519;
14 months ago, by wenzelm
proper formatting;
14 months ago, by wenzelm
more documentation on "isabelle build -H" and underlying system registry tables "host" and "cluster";
14 months ago, by wenzelm
More binomial material
14 months ago, by paulson
syntax of gchoose now the same as choose
14 months ago, by paulson
Some new simprules – and patches for proofs
15 months ago, by paulson
merged
15 months ago, by paulson
merged
15 months ago, by paulson
A little more tidying in Nominal
15 months ago, by paulson
tuned proofs;
15 months ago, by wenzelm
merged, resoving conflicts in src/HOL/Nominal/Nominal.thy;
15 months ago, by wenzelm
Added tag Isabelle2024-RC3 for changeset 007e6af8a020
15 months ago, by wenzelm
more documentation on "System registry via TOML";
15 months ago, by wenzelm
update to naproche-20240502: proper platform_path for NAPROCHE_FORMALIZATIONS to make it work on Windows;
15 months ago, by wenzelm
provide 3.1 for testing (inactive);
15 months ago, by wenzelm
build e-3.1, without patch;
15 months ago, by wenzelm
disable Isabelle/Naproche for now: does not quite work on Windows;
15 months ago, by wenzelm
update and activate naproche component for release;
15 months ago, by wenzelm
changed URL to SystemOnTPTP at Geoff's request
15 months ago, by desharna
tuned spelling;
15 months ago, by wenzelm
build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state;
15 months ago, by wenzelm
proper directory permissions to make "rm" work, notably for cygwin/etc/pki/ca-trust/extracted/pem/directory-hash;
15 months ago, by wenzelm
support more Ubuntu versions;
15 months ago, by wenzelm
updated for release;
15 months ago, by wenzelm
more robust: avoid spurious ConcurrentModificationException;
15 months ago, by wenzelm
update to e-3.0.03-1, with proper support for trivial statements;
15 months ago, by wenzelm
more robust;
15 months ago, by wenzelm
minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements;
15 months ago, by wenzelm
backed out changeset 601ff5c7cad5: not relevant for Isabelle2024;
15 months ago, by wenzelm
clone of 0c51e0a6bc37;
15 months ago, by wenzelm
update Windows test machines;
15 months ago, by wenzelm
More tidying of proofs
15 months ago, by paulson
Another Nominal example
15 months ago, by paulson
merged
15 months ago, by paulson
Tidying up another Nominal example (SOS)
15 months ago, by paulson
update Windows build host;
15 months ago, by wenzelm
proper command-line;
15 months ago, by wenzelm
Tidying up another of the nominal examples
15 months ago, by paulson
More tidying of Nominal proofs
15 months ago, by paulson
Tidied up another messy theory
15 months ago, by paulson
More proof tidying for Nominal
15 months ago, by paulson
Tidying up more messy proofs
15 months ago, by paulson
Starting to tidy HOL-Nominal-Examples
15 months ago, by paulson
sketch & explore: recover from duplicate fixed variables in Isar proofs
15 months ago, by Simon Wimmer
back to post-release mode -- after fork point;
15 months ago, by wenzelm
merged
15 months ago, by wenzelm
Added tag Isabelle2024-RC2 for changeset ef2134570abb
15 months ago, by wenzelm
Acknowledgement of Ata Keskin for his Martingales material
15 months ago, by paulson
merged
15 months ago, by wenzelm
update to jdk-21.0.3;
15 months ago, by wenzelm
merged
15 months ago, by paulson
Tidied up horrible archaic proofs
15 months ago, by paulson
clarified signature;
15 months ago, by wenzelm
make adhoc_overloading respect type constraints
15 months ago, by Kevin Kappelmann
merged
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
minor performance tuning: avoid redundant server access;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
clarified modules and options (from store);
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
15 months ago, by wenzelm
tuned messages;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
back to static numa_nodes (reverting part of c2c59de57df9);
15 months ago, by wenzelm
tuned messages;
15 months ago, by wenzelm
canonical time function for List.nth
15 months ago, by Manuel Eberl
merged
15 months ago, by paulson
Streamlining of many more archaic proofs
15 months ago, by paulson
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
15 months ago, by Fabian Huch
More tidying of old proofs
15 months ago, by paulson
merged
15 months ago, by paulson
More tidying and removal of "apply"
15 months ago, by paulson
Add subgoals variant of 'sketch' command
15 months ago, by Simon Wimmer
merged
15 months ago, by paulson
Tidied some messy proofs
15 months ago, by paulson
prefer canonical theorem name for fact collection declarations
15 months ago, by haftmann
merged
15 months ago, by paulson
Tidying ugly proofs
15 months ago, by paulson
tuned;
15 months ago, by Fabian Huch
tweaked time functions for median-of-medians selection in HOL-Data_Structures
15 months ago, by Manuel Eberl
merged
15 months ago, by wenzelm
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta;
15 months ago, by wenzelm
Tiny tweaks to proofs
15 months ago, by paulson
A bit of new material about type class "infinite", from Eval_FO
15 months ago, by paulson
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
16 months ago, by wenzelm
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
16 months ago, by wenzelm
adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;
16 months ago, by wenzelm
Add entry on Sketch_and_Explore to CONTRIBUTORS
16 months ago, by Simon Wimmer
moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
16 months ago, by Manuel Eberl
more portable: prefer official JDBC operation DatabaseMetaData.getColumns();
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
documented new syntax for fBall and fBex
16 months ago, by desharna
updated for release;
16 months ago, by wenzelm
Added tag Isabelle2024-RC1 for changeset 1231a7fb2510
16 months ago, by wenzelm
misc tuning for release;
16 months ago, by wenzelm
update for release;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
update to stack-2.15.5, stackage-lts-22.15;
16 months ago, by wenzelm
clarified names: discontinue odd convention from 3 decades ago;
16 months ago, by wenzelm
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;
16 months ago, by wenzelm
added documentation for meromorphicity etc. in HOL-Complex_Analysis
16 months ago, by Manuel Eberl
merged
16 months ago, by desharna
merged
16 months ago, by desharna
added special syntax for FSet.Ball and FSet.Bex
16 months ago, by desharna
tuned proof
16 months ago, by desharna
tuned proofs of Equiv_Relations.equiv
16 months ago, by desharna
remove transitional (dummy) component list for Go
16 months ago, by Lars Hupel
clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;
16 months ago, by wenzelm
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
16 months ago, by wenzelm
provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;
16 months ago, by wenzelm