isabelle: Graph

more general ML_Antiquotation.special_form;
19 months ago, by wenzelm
Importing or moving a few more useful theorems
19 months ago, by paulson
merged
19 months ago, by paulson
A few new theorems
19 months ago, by paulson
avoid legacy binding errors in Sledgehammer Isar proofs
19 months ago, by blanchet
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
19 months ago, by blanchet
added argo
19 months ago, by blanchet
allow (~) syntax in TPTP proofs for unapplied negation
19 months ago, by blanchet
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
19 months ago, by blanchet
use same associativity as Isabelle when parsing HOL proofs
19 months ago, by blanchet
improved Sledgehammer's HOL proof parser w.r.t. negation
19 months ago, by blanchet
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
minor performance tuning;
19 months ago, by wenzelm
merged
19 months ago, by paulson
A few new or simplified proofs
19 months ago, by paulson
tuned: more standard order;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
proper fontenc for cartouches (amending d052d61da398);
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
more robust: prefer linear data flow;
19 months ago, by wenzelm
added first proof reconstruction test for Sledgehammer
19 months ago, by desharna
tuned;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature (again): follow Isabelle/Java/Scala;
19 months ago, by wenzelm
tuned (following 69c6d3e87660);
19 months ago, by wenzelm
tuned --- avoid pointless indirection (see also a2df9de46060);
19 months ago, by wenzelm
(pointlessly) get rid of some simp calls within "proof"
20 months ago, by paulson
reduced prominence of lemma names
20 months ago, by haftmann
new formulation of an auxiliary lemma
20 months ago, by haftmann
A few more inclusion-exclusion theorems from HOL Light
20 months ago, by paulson
Corrected type calculation.
20 months ago, by haftmann
some hints on managed installations
20 months ago, by haftmann
prefer cartouches over quotes for clarity of resulting document
20 months ago, by haftmann
A little reorganisation
20 months ago, by paulson
post-release updates;
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
Added tag Isabelle2023 for changeset b5f3d1051b13
20 months ago, by wenzelm
tuned; Isabelle2023
20 months ago, by wenzelm
misc tuning;
20 months ago, by wenzelm
documentation for the "Document" panel in Isabelle/jEdit;
20 months ago, by wenzelm
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
20 months ago, by paulson
merged
20 months ago, by paulson
merged
20 months ago, by paulson
tidying up old apply-style proofs
20 months ago, by paulson
allow higher-order unification of open terms (reviewed by Larry Paulson)
20 months ago, by Kevin Kappelmann
merged
20 months ago, by wenzelm
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
20 months ago, by wenzelm
add ML_system_pp for type Isabelle_Thread.T;
20 months ago, by wenzelm
more explicit type Isabelle_Thread.T;
20 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);
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
tuned Sledgehammer messages
20 months ago, by blanchet
respect timeout better
20 months ago, by blanchet
merged
20 months ago, by wenzelm
Added tag Isabelle2023-RC5 for changeset ffa417b5c913
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned messages;
20 months ago, by wenzelm
proper stop of build_process shutdown, despite errors on workers;
20 months ago, by wenzelm
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
20 months ago, by wenzelm
support "isabelle build_worker -q";
20 months ago, by wenzelm
support "isabelle build_process -r -f";
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified output;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature: removed ununsed option;
20 months ago, by wenzelm
tuned message;
20 months ago, by wenzelm
updated to naproche-20230902: add examples/100_theorems.ftl.tex and some more text in Isabelle/Intro.thy;
20 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;
20 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);
20 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
20 months ago, by wenzelm
more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;
20 months ago, by wenzelm
more accurate documentation of record field update, following changes in Isabelle2007 and Isabelle2008;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
more robust: "hostname" command might be absent, notably on Arch Linux (and other systemd-based distributions);
20 months ago, by wenzelm
tuned NEWS;
20 months ago, by wenzelm
NEWS;
20 months ago, by wenzelm
update to "scalac -source 3.3" (from 3.1);
20 months ago, by wenzelm
proper pattern (amending ff86f10e54cd);
20 months ago, by wenzelm
discontinue odd AFP partitioning: let Build_Cluster / Build_Engine do the job;
20 months ago, by wenzelm
discontinue special treatment of AFP: "isabelle dump" has been superseded by regular "isabelle build" databases;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
proper type, following Bus.event;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
tuned indentation;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified signature: prefer enum types;
20 months ago, by wenzelm
clarified generated Scala, for the sake of "scalac -source 3.3";
20 months ago, by wenzelm
discontinue old Java 11 LTS;
20 months ago, by wenzelm
misc tuning: support "scalac -source 3.3";
20 months ago, by wenzelm
obsolete (see b4e6b82fdb9e);
20 months ago, by wenzelm
merged
20 months ago, by wenzelm
update for release;
20 months ago, by wenzelm
Added tag Isabelle2023-RC4 for changeset 12aac1489f3b
20 months ago, by wenzelm
minimal documentation for build cluster support;
20 months ago, by wenzelm
more robust access to local variables;
20 months ago, by wenzelm
tuned messages: avoid duplicates;
20 months ago, by wenzelm
removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
20 months ago, by wenzelm
tuned error;
20 months ago, by wenzelm
tuned messages (again);
20 months ago, by wenzelm
tuned: prefer explicit types;
20 months ago, by wenzelm
support for Host.dirs;
20 months ago, by wenzelm
tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;
20 months ago, by wenzelm
support multiple host names;
20 months ago, by wenzelm
clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;
20 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
20 months ago, by blanchet
tuned message;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
more accurate treatment of state vs. serial vs. db;
20 months ago, by wenzelm
more explicit check;
20 months ago, by wenzelm
proper numa_nodes for build_worker;
20 months ago, by wenzelm
tuned message;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
support hosts with shared directory (e.g. NFS);
20 months ago, by wenzelm
tuned message: failure may stem from build_cluster init;
20 months ago, by wenzelm
proper sync_database for receive timeout;
20 months ago, by wenzelm
clarified source structure;
20 months ago, by wenzelm
tuned whitespace;
20 months ago, by wenzelm
clarified command-line tools;
20 months ago, by wenzelm
tuned output;
20 months ago, by wenzelm
clarified signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
tuned signature;
20 months ago, by wenzelm
proper sequential evaluation;
20 months ago, by wenzelm
more robust command options;
20 months ago, by wenzelm
performance tuning: avoid redundant db access;
20 months ago, by wenzelm
clarified signature: proper treatment of implicit state (amending d0c9d277620e);
20 months ago, by wenzelm
performance tuning: avoid redundant db access;
20 months ago, by wenzelm
performance tuning: avoid multiple db roundtrips;
20 months ago, by wenzelm
clarified signature: more robust treatment of implicit state;
20 months ago, by wenzelm
proper sync_database for Database_Progress consumer;
20 months ago, by wenzelm
tuned message;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
tuned messages;
20 months ago, by wenzelm
tuned signature: removed unused arguments;
20 months ago, by wenzelm
minor performance tuning: avoid multiple db roundtrips;
20 months ago, by wenzelm
more operations;
20 months ago, by wenzelm
tuned;
20 months ago, by wenzelm
limit size and complexity of bulk transactions;
20 months ago, by wenzelm
more scalable write_entries and Export.consumer via db.execute_batch_statement;
20 months ago, by wenzelm
clarified signature: filter batch;
20 months ago, by wenzelm
more scalable write_messages via db.execute_batch_statement;
20 months ago, by wenzelm
support for execute_batch: multiple statements in one round-trip;
20 months ago, by wenzelm
more robust;
21 months ago, by wenzelm
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
21 months ago, by wenzelm
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
21 months ago, by wenzelm
clarified main_loop: support timeout, which results in consume(Nil);
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
clarified signature;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
build_worker is stopped independently from master build_process;
21 months ago, by wenzelm
clarified command arguments: optionally restrict to given theories (from theory loader);
21 months ago, by wenzelm
tuned signature: more operations for formal theory context vs. theory loader;
21 months ago, by wenzelm
added Isar command 'print_context_tracing';
21 months ago, by wenzelm
avoid confusion: this is merely about "isabelle dotnet_setup", no codegen yet;
21 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
20 months ago, by blanchet
merged
20 months ago, by paulson
some refinements in Algebra and Number_Theory
20 months ago, by paulson
provide Go component
20 months ago, by Lars Hupel
merged
20 months ago, by paulson
A subtle fix involving the "measurable" attribute
20 months ago, by paulson
merged
20 months ago, by paulson
Numerous minor tweaks and simplifications
20 months ago, by paulson
substantial tidy-up, shortening many proofs
21 months ago, by paulson
add Go component
20 months ago, by Lars Hupel
backed out changeset 2a26d423d9fb: build_log_database not run yet, so this tests the same changesets again;
21 months ago, by wenzelm
back to post-release mode -- after fork point;
21 months ago, by wenzelm
Added tag Isabelle2023-RC3 for changeset f5fb5bb2533f
21 months ago, by wenzelm
clarified option name (see also ff43a524aa5d);
21 months ago, by wenzelm
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
21 months ago, by wenzelm
more robust: atomic file-system result via tmp file;
21 months ago, by wenzelm
removed junk (amending 8cd399b25dac);
21 months ago, by wenzelm
more robust wrt. undefined state;
21 months ago, by wenzelm
more informative error;
21 months ago, by wenzelm
more robust;
21 months ago, by wenzelm
tuned signature;
21 months ago, by wenzelm
clarified signature: more explicit types;
21 months ago, by wenzelm
more informative shasum: show differences explicitly;
21 months ago, by wenzelm
tuned messages;
21 months ago, by wenzelm
more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere;
21 months ago, by wenzelm
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
21 months ago, by wenzelm
merged
21 months ago, by nipkow
improved simp rule insert_Times_insert (following Dominique Unruh).
21 months ago, by nipkow
afford multiple tests for arm64_32-darwin on this fast machine;
21 months ago, by wenzelm
proper history_base for AMR64;
21 months ago, by wenzelm
tuned
21 months ago, by nipkow
more robust support for ARM64 platform;
21 months ago, by wenzelm
proper support for Apple Silicon (ARM64);
21 months ago, by wenzelm
merged
21 months ago, by wenzelm
tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
21 months ago, by wenzelm
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
21 months ago, by wenzelm
proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
21 months ago, by wenzelm
made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
21 months ago, by traytel
made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
21 months ago, by traytel
systematic testing of arm64_32-darwin;
21 months ago, by wenzelm
more hardware details;
21 months ago, by wenzelm
update to polyml-219e0a248f70, with more robust support for ARM64;
21 months ago, by wenzelm
tuned generated README;
21 months ago, by wenzelm
merged
21 months ago, by paulson
Tidied up more messy proofs
21 months ago, by paulson
hints on "hg bisect";
21 months ago, by wenzelm
no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
21 months ago, by wenzelm
Removal of ugly old proofs
21 months ago, by paulson
merged
21 months ago, by paulson
More cosmetic changes
21 months ago, by paulson
Cosmetic polishing of proofs
21 months ago, by paulson
remove debug printing
21 months ago, by Mathias Fleury
merged
21 months ago, by nipkow
added mbox-like latex sugar
21 months ago, by nipkow
Added tag Isabelle2023-RC2 for changeset 53b59fa42696
21 months ago, by wenzelm
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
21 months ago, by wenzelm
revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
21 months ago, by wenzelm
output panel: don't discard already filtered messages
21 months ago, by kleing
merged
21 months ago, by wenzelm
tuned signature: more operations;
21 months ago, by wenzelm
avoid excessive accumulation of garbage, for profiling of huge sessions;
21 months ago, by wenzelm
clarified signature: systematic use of Properties.make_string;
21 months ago, by wenzelm
tuned;
21 months ago, by wenzelm
support for let in Alethe name bindings;
21 months ago, by Mathias Fleury
merged
21 months ago, by paulson
A few more cosmetic changes to proofs
21 months ago, by paulson
merged
22 months ago, by paulson
tidying a few proofs a bit more
22 months ago, by paulson
partly tidied some truly horrible proofs
22 months ago, by paulson
update for release;
21 months ago, by wenzelm
back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool;
21 months ago, by wenzelm
performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);
21 months ago, by wenzelm
clarified statistics;
21 months ago, by wenzelm
show more build history for AFP;
21 months ago, by wenzelm
more statistics;
21 months ago, by wenzelm
proper base_thys;
21 months ago, by wenzelm
more thorough context tracing;
21 months ago, by wenzelm
proper check;
21 months ago, by wenzelm
proper symbolic hostname, as provided via Build_Cluster.Host;
21 months ago, by wenzelm