isabelle: Graph

tuned signature: more operations;
15 months ago, by wenzelm
more specific name for type class
15 months ago, by haftmann
proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified modules;
15 months ago, by wenzelm
clarified signature: more operations;
15 months ago, by wenzelm
tuned comments;
15 months ago, by wenzelm
more NEWS;
15 months ago, by wenzelm
more TODO;
15 months ago, by wenzelm
prefer strict test of system options;
15 months ago, by wenzelm
some build cluster resources at TUM;
15 months ago, by wenzelm
build cluster host specifications are based on registry entries (table prefix "host");
15 months ago, by wenzelm
more robust init;
15 months ago, by wenzelm
clarified signature: more operations;
15 months ago, by wenzelm
support interpreted/typed entries via Registry.Category and Registry.Table;
15 months ago, by wenzelm
clarified signature: more operations;
15 months ago, by wenzelm
clarified output;
15 months ago, by wenzelm
support for global registry;
15 months ago, by wenzelm
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";
15 months ago, by wenzelm
slightly less technical formulation of very specific type class
15 months ago, by haftmann
weakened dependency
15 months ago, by haftmann
explicit type class for discrete linordered semidoms
15 months ago, by haftmann
proper dummy timing entries;
15 months ago, by Fabian Huch
use only finished sessions in timing data;
15 months ago, by Fabian Huch
tuned;
15 months ago, by Fabian Huch
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
15 months ago, by Fabian Huch
performance tuning for build schedule: faster stopping;
15 months ago, by Fabian Huch
performance tuning for timing heuristic: pre-calculate graph operations;
15 months ago, by Fabian Huch
move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
15 months ago, by Fabian Huch
clarified signature: emphasize mutable instance;
15 months ago, by wenzelm
clarified signature: more operations;
15 months ago, by wenzelm
support for explicit SSH hostname;
15 months ago, by wenzelm
proper local host (amending 62d7ef1da441);
15 months ago, by wenzelm
merged
15 months ago, by nipkow
added lemma
15 months ago, by nipkow
proper default for disjunction (amending 9f7a94117666);
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
more operations;
15 months ago, by wenzelm
avoid option -C: free this latter for build-related configuration;
15 months ago, by wenzelm
more direct indentation, using Symbol.spaces;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
more accurate treatment of surrounding whitespace;
15 months ago, by wenzelm
obsolete (see also f627ab8c276c);
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
15 months ago, by wenzelm
clarified modules;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);
15 months ago, by wenzelm
more tests;
15 months ago, by wenzelm
clarified exploration of history: more uniform options;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
enable multi-builds (again, see also 0c7419d3dd59);
15 months ago, by wenzelm
explore history more thoroughly;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
clarified "recent" time: days <= 0 means infinity (no constraint);
15 months ago, by wenzelm
tuned whitespace;
15 months ago, by wenzelm
proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda);
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
tuned output;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned message;
15 months ago, by wenzelm
proper option;
15 months ago, by wenzelm
merged
15 months ago, by wenzelm
proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1;
15 months ago, by wenzelm
Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
15 months ago, by paulson
merged
15 months ago, by wenzelm
prefer Time.scale(), following Isabelle/ML;
15 months ago, by wenzelm
proper benchmark command;
15 months ago, by Fabian Huch
merged
15 months ago, by wenzelm
proper progress (see also 45d570945fe4);
15 months ago, by wenzelm
improved build messages;
15 months ago, by Fabian Huch
clarified;
15 months ago, by Lukas Stevens
merged
15 months ago, by paulson
fixed the simplification of Suc n - 1
15 months ago, by paulson
tuned whitespace;
15 months ago, by wenzelm
tuned message;
15 months ago, by wenzelm
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
15 months ago, by wenzelm
more detailed progress for build_log_database, to see better what happens when;
15 months ago, by wenzelm
clarified signature: explicit Progress date;
15 months ago, by wenzelm
more uniform progress;
15 months ago, by wenzelm
more robust: support concurrent output;
15 months ago, by wenzelm
disable multi-builds (again): does not quite work yet;
15 months ago, by wenzelm
clarified modules;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
proper Compress.Cache;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
15 months ago, by wenzelm
support for mailbox limit;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
15 months ago, by wenzelm
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
15 months ago, by wenzelm
afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb);
15 months ago, by wenzelm
performance tuning: parallel and incremental update of build_log_database;
15 months ago, by wenzelm
performance tuning: more careful database access;
15 months ago, by wenzelm
clarified message;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
prefer old-style import "=>";
15 months ago, by wenzelm
merged
15 months ago, by wenzelm
redundant (see also 3069da1743bc);
15 months ago, by wenzelm
removed obsolete table (see also 6acd1a2bd146);
15 months ago, by wenzelm
more robust init_database();
15 months ago, by wenzelm
proper private_data.transaction_lock;
15 months ago, by wenzelm
clarified names;
15 months ago, by wenzelm
proper support for SSH;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
tuned imports;
15 months ago, by wenzelm
add module for faster scheduled builds;
16 months ago, by Fabian Huch
always use host database and make protected;
16 months ago, by Fabian Huch
read relative cpu from build log;
16 months ago, by Fabian Huch
prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);
16 months ago, by Fabian Huch
added start date to build jobs, e.g., for build time estimation;
16 months ago, by Fabian Huch
added initial version of benchmark module, e.g., to compare performance of different hosts;
16 months ago, by Fabian Huch
generalized node infos: allow addressing of numa node segments via relative cpus;
16 months ago, by Fabian Huch
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
16 months ago, by Fabian Huch
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
16 months ago, by Fabian Huch
defined statically known tables of Build_Log;
16 months ago, by Fabian Huch
added lemma
15 months ago, by nipkow
added lemma
15 months ago, by nipkow
added lemma
15 months ago, by nipkow
NEWS and CONTRIBUTORS;
15 months ago, by Fabian Huch
remove unused ci-extras component;
15 months ago, by Fabian Huch
use mail module in CI build;
15 months ago, by Fabian Huch
added mail module;
15 months ago, by Fabian Huch
build javamail component and add to main components;
15 months ago, by Fabian Huch
added component for javax mail;
15 months ago, by Fabian Huch
updated to vampire-4.8;
15 months ago, by wenzelm
tuned README;
15 months ago, by wenzelm
update Vampire version, following hints by Martin Desharnais;
15 months ago, by wenzelm
removed junk;
15 months ago, by wenzelm
tuned component_vampire script for Vampire 4.8 and added new flag to force version name
16 months ago, by desharna
prefer Isabelle options for CI mail settings over ci.properties;
15 months ago, by Fabian Huch
Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.
15 months ago, by paulson
proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);
15 months ago, by wenzelm
unused (see fe9e590ae52f);
15 months ago, by wenzelm
clarified modules;
15 months ago, by wenzelm
merged
15 months ago, by wenzelm
update documentation on simproc_setup;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper morphism;
16 months ago, by wenzelm
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
16 months ago, by wenzelm
more compact ML source;
16 months ago, by wenzelm
more robust read_simproc_spec: proper error positions;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
16 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
16 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
16 months ago, by wenzelm
added ML antiquotation "simproc_setup";
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified syntax and order of parameters;
16 months ago, by wenzelm
clarified signature: Named_Target.setup works both for global and local theory;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature: more concise simproc setup in ML;
16 months ago, by wenzelm
clarified signature: more concise variations on implicit theory setup;
16 months ago, by wenzelm
clarified simproc_setup (passive);
16 months ago, by wenzelm
clarified 'simproc_setup';
16 months ago, by wenzelm
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
16 months ago, by wenzelm
more standard simproc_setup in Isar;
16 months ago, by wenzelm
more standard ML setup;
16 months ago, by wenzelm
proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0
16 months ago, by desharna
added new portfolio for Vampire 4.8
16 months ago, by desharna
tuned signature, following Isabelle/Scala;
16 months ago, by wenzelm
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper parallel build tasks;
16 months ago, by wenzelm
more Haskell tests on macOS;
16 months ago, by wenzelm
more NEWS;
16 months ago, by wenzelm
disable naproche component for now: to be updated before the next Isabelle release;
16 months ago, by wenzelm
updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell");
16 months ago, by wenzelm
more NEWS;
16 months ago, by wenzelm
tuned structure;
16 months ago, by wenzelm
update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
16 months ago, by wenzelm
updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur;
16 months ago, by wenzelm
proper options for macOS 11 Big Sur;
16 months ago, by wenzelm
support for official release of polyml-5.9.1;
16 months ago, by wenzelm
updated Linux baseline to Ubuntu 18.04;
16 months ago, by wenzelm
support for macOS 14 Sonoma (only for testing);
16 months ago, by wenzelm
more platform tests: initial support for macOS 14 Sonoma;
16 months ago, by wenzelm
updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
16 months ago, by wenzelm
clarified user errors vs. failures, e.g. java.lang.StackOverflowError;
16 months ago, by wenzelm
further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;
16 months ago, by wenzelm
proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
16 months ago, by wenzelm
distinguish proper interrupts from Poly/ML RTS breakdown;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper Isabelle_Thread.try_catch;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
proper Exn.capture / Isabelle_Thread.try_catch;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
proper Exn.capture;
16 months ago, by wenzelm
more robust: avoid race condition;
16 months ago, by wenzelm
clarified name;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified comments;
16 months ago, by wenzelm
Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts
16 months ago, by paulson
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
16 months ago, by paulson
merged
16 months ago, by paulson
New proofs also some slightly faster existing proofs
16 months ago, by paulson
updated to hugo-0.119.0;
16 months ago, by Fabian Huch
add component build tool for hugo from afp-devel;
16 months ago, by Fabian Huch
removed test failing on some platform
16 months ago, by desharna
mini2 is not active due to upgrade;
16 months ago, by wenzelm
more PLATFORMS;
16 months ago, by wenzelm
update documentation on Isabelle/ML exceptions;
16 months ago, by wenzelm
misc tuning;
16 months ago, by wenzelm
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
16 months ago, by wenzelm
proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);
16 months ago, by wenzelm
proper Scala version, e.g. for IntelliJ IDEA;
16 months ago, by wenzelm
NEWS
16 months ago, by desharna
used standard Time.compare in Sledgehammer's preplay
16 months ago, by desharna
moved variable bindings to tighter scope
16 months ago, by desharna
removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer
16 months ago, by desharna
removed unused function parameter
16 months ago, by desharna
merged
16 months ago, by paulson
A couple of new lemmas
16 months ago, by paulson
merged
16 months ago, by wenzelm
more NEWS;
16 months ago, by wenzelm
explicitly reject 'handle' with catch-all patterns;
16 months ago, by wenzelm
avoid accidental 'handle' of interrupts;
16 months ago, by wenzelm
tuned: prefer try-catch/finally over low-level 'handle';
16 months ago, by wenzelm
clarified treatment of exceptions: avoid catch-all handlers;
16 months ago, by wenzelm
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
more robust management of resources, using Thread_Attributes.uninterruptible;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
more robust management of resources, using Thread_Attributes.uninterruptible;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned signature;
16 months ago, by wenzelm
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
unused;
16 months ago, by wenzelm
clarified order of modules: early access to interrupt management of Isabelle_Threads;
16 months ago, by wenzelm
tuned: prefer antiquotation for try-catch;
16 months ago, by wenzelm
tuned: prefer antiquotation for try-catch;
16 months ago, by wenzelm
tuned: prefer antiquotation for try-finally;
16 months ago, by wenzelm
omit pointless capture/release (see also 469a375212c1);
16 months ago, by wenzelm
omit pointless capture/release (see also 26774ccb1c74);
16 months ago, by wenzelm
clarified signature: avoid association with potentially dangerous Exn.capture;
16 months ago, by wenzelm
more robust: catch/finally part is uninterruptible;
16 months ago, by wenzelm
more position information, e.g. for warning about fn-pattern;
16 months ago, by wenzelm
unused;
16 months ago, by wenzelm
more general ML_Antiquotation.special_form;
16 months ago, by wenzelm
Importing or moving a few more useful theorems
16 months ago, by paulson
merged
16 months ago, by paulson
A few new theorems
16 months ago, by paulson
avoid legacy binding errors in Sledgehammer Isar proofs
16 months ago, by blanchet
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
16 months ago, by blanchet
added argo
16 months ago, by blanchet
allow (~) syntax in TPTP proofs for unapplied negation
16 months ago, by blanchet
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
16 months ago, by blanchet
use same associativity as Isabelle when parsing HOL proofs
16 months ago, by blanchet
improved Sledgehammer's HOL proof parser w.r.t. negation
16 months ago, by blanchet
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
minor performance tuning;
16 months ago, by wenzelm
merged
16 months ago, by paulson
A few new or simplified proofs
16 months ago, by paulson
tuned: more standard order;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
proper fontenc for cartouches (amending d052d61da398);
17 months ago, by wenzelm
clarified modules;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
clarified modules;
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
more robust: prefer linear data flow;
17 months ago, by wenzelm
added first proof reconstruction test for Sledgehammer
17 months ago, by desharna
tuned;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
clarified signature (again): follow Isabelle/Java/Scala;
17 months ago, by wenzelm
tuned (following 69c6d3e87660);
17 months ago, by wenzelm
tuned --- avoid pointless indirection (see also a2df9de46060);
17 months ago, by wenzelm
(pointlessly) get rid of some simp calls within "proof"
17 months ago, by paulson
reduced prominence of lemma names
17 months ago, by haftmann
new formulation of an auxiliary lemma
17 months ago, by haftmann
A few more inclusion-exclusion theorems from HOL Light
17 months ago, by paulson
Corrected type calculation.
17 months ago, by haftmann
some hints on managed installations
17 months ago, by haftmann
prefer cartouches over quotes for clarity of resulting document
17 months ago, by haftmann
A little reorganisation
17 months ago, by paulson
post-release updates;
17 months ago, by wenzelm
merged
17 months ago, by wenzelm
Added tag Isabelle2023 for changeset b5f3d1051b13
17 months ago, by wenzelm
tuned; Isabelle2023
17 months ago, by wenzelm
misc tuning;
17 months ago, by wenzelm
documentation for the "Document" panel in Isabelle/jEdit;
17 months ago, by wenzelm
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
17 months ago, by paulson
merged
17 months ago, by paulson
merged
17 months ago, by paulson
tidying up old apply-style proofs
17 months ago, by paulson
allow higher-order unification of open terms (reviewed by Larry Paulson)
17 months ago, by Kevin Kappelmann
merged
17 months ago, by wenzelm
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
17 months ago, by wenzelm
add ML_system_pp for type Isabelle_Thread.T;
17 months ago, by wenzelm
more explicit type Isabelle_Thread.T;
17 months ago, by wenzelm
discontinue somewhat pointless thread tracing/debugging: without PIDE command context, messages are not shown, and Exn.trace hardly works anyway (see also de20fccf6509 and 447972249785);
17 months ago, by wenzelm
tuned whitespace;
17 months ago, by wenzelm
tuned Sledgehammer messages
17 months ago, by blanchet
respect timeout better
17 months ago, by blanchet
merged
17 months ago, by wenzelm
Added tag Isabelle2023-RC5 for changeset ffa417b5c913
17 months ago, by wenzelm
tuned;
17 months ago, by wenzelm
tuned messages;
17 months ago, by wenzelm
proper stop of build_process shutdown, despite errors on workers;
17 months ago, by wenzelm
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
17 months ago, by wenzelm
support "isabelle build_worker -q";
17 months ago, by wenzelm
support "isabelle build_process -r -f";
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
clarified output;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
clarified signature: removed ununsed option;
17 months ago, by wenzelm
tuned message;
17 months ago, by wenzelm
updated to naproche-20230902: add examples/100_theorems.ftl.tex and some more text in Isabelle/Intro.thy;
17 months ago, by wenzelm
more robust access to output file of external smt, notably for Windows 11, where transient ERROR_SHARING_VIOLATION has been seen;
17 months ago, by wenzelm
more robust $ISABELLE_TMP_PREFIX on windows: avoid location within Cygwin root, i.e. inside the program directory (see also ff92d6edff2c and 1df53737c59b);
17 months ago, by wenzelm
more robust $TMPDIR on windows, e.g. for repository snapshot: do not depend on $TEMP_WINDOWS provided by official distribution;a
17 months ago, by wenzelm
more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;
17 months ago, by wenzelm
more accurate documentation of record field update, following changes in Isabelle2007 and Isabelle2008;
17 months ago, by wenzelm
tuned whitespace;
17 months ago, by wenzelm
more robust: "hostname" command might be absent, notably on Arch Linux (and other systemd-based distributions);
17 months ago, by wenzelm
tuned NEWS;
17 months ago, by wenzelm
NEWS;
17 months ago, by wenzelm
update to "scalac -source 3.3" (from 3.1);
17 months ago, by wenzelm
proper pattern (amending ff86f10e54cd);
17 months ago, by wenzelm
discontinue odd AFP partitioning: let Build_Cluster / Build_Engine do the job;
17 months ago, by wenzelm
discontinue special treatment of AFP: "isabelle dump" has been superseded by regular "isabelle build" databases;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
proper type, following Bus.event;
17 months ago, by wenzelm
clarified signature;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
tuned indentation;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified signature: prefer enum types;
17 months ago, by wenzelm
clarified generated Scala, for the sake of "scalac -source 3.3";
17 months ago, by wenzelm
discontinue old Java 11 LTS;
17 months ago, by wenzelm
misc tuning: support "scalac -source 3.3";
17 months ago, by wenzelm
obsolete (see b4e6b82fdb9e);
17 months ago, by wenzelm
merged
17 months ago, by wenzelm
update for release;
17 months ago, by wenzelm
Added tag Isabelle2023-RC4 for changeset 12aac1489f3b
17 months ago, by wenzelm
minimal documentation for build cluster support;
17 months ago, by wenzelm
more robust access to local variables;
17 months ago, by wenzelm
tuned messages: avoid duplicates;
17 months ago, by wenzelm
removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
17 months ago, by wenzelm
tuned error;
17 months ago, by wenzelm
tuned messages (again);
17 months ago, by wenzelm
tuned: prefer explicit types;
17 months ago, by wenzelm
support for Host.dirs;
17 months ago, by wenzelm
tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;
17 months ago, by wenzelm
support multiple host names;
17 months ago, by wenzelm
clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;
17 months ago, by wenzelm
avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer
17 months ago, by blanchet
tuned message;
17 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
more accurate treatment of state vs. serial vs. db;
18 months ago, by wenzelm