isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -112 +112 +1000 +3000 tip

avoid accidental 'handle' of interrupts;
15 months ago, by wenzelm
tuned: prefer try-catch/finally over low-level 'handle';
15 months ago, by wenzelm
clarified treatment of exceptions: avoid catch-all handlers;
15 months ago, by wenzelm
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
more robust management of resources, using Thread_Attributes.uninterruptible;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
more robust management of resources, using Thread_Attributes.uninterruptible;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified modules;
15 months ago, by wenzelm
unused;
15 months ago, by wenzelm
clarified order of modules: early access to interrupt management of Isabelle_Threads;
15 months ago, by wenzelm
tuned: prefer antiquotation for try-catch;
15 months ago, by wenzelm
tuned: prefer antiquotation for try-catch;
15 months ago, by wenzelm
tuned: prefer antiquotation for try-finally;
15 months ago, by wenzelm
omit pointless capture/release (see also 469a375212c1);
15 months ago, by wenzelm
omit pointless capture/release (see also 26774ccb1c74);
15 months ago, by wenzelm
clarified signature: avoid association with potentially dangerous Exn.capture;
15 months ago, by wenzelm
more robust: catch/finally part is uninterruptible;
15 months ago, by wenzelm
more position information, e.g. for warning about fn-pattern;
15 months ago, by wenzelm
unused;
15 months ago, by wenzelm
more general ML_Antiquotation.special_form;
15 months ago, by wenzelm
Importing or moving a few more useful theorems
15 months ago, by paulson
merged
15 months ago, by paulson
A few new theorems
15 months ago, by paulson
avoid legacy binding errors in Sledgehammer Isar proofs
15 months ago, by blanchet
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
15 months ago, by blanchet
added argo
15 months ago, by blanchet
allow (~) syntax in TPTP proofs for unapplied negation
15 months ago, by blanchet
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
15 months ago, by blanchet
use same associativity as Isabelle when parsing HOL proofs
15 months ago, by blanchet
improved Sledgehammer's HOL proof parser w.r.t. negation
15 months ago, by blanchet
clarified signature;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
minor performance tuning;
15 months ago, by wenzelm
merged
15 months ago, by paulson
A few new or simplified proofs
15 months ago, by paulson
tuned: more standard order;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
proper fontenc for cartouches (amending d052d61da398);
15 months ago, by wenzelm
clarified modules;
15 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified modules;
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
more robust: prefer linear data flow;
16 months ago, by wenzelm
added first proof reconstruction test for Sledgehammer
16 months ago, by desharna
tuned;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature (again): follow Isabelle/Java/Scala;
16 months ago, by wenzelm
tuned (following 69c6d3e87660);
16 months ago, by wenzelm
tuned --- avoid pointless indirection (see also a2df9de46060);
16 months ago, by wenzelm
(pointlessly) get rid of some simp calls within "proof"
16 months ago, by paulson
reduced prominence of lemma names
16 months ago, by haftmann
new formulation of an auxiliary lemma
16 months ago, by haftmann
A few more inclusion-exclusion theorems from HOL Light
16 months ago, by paulson
Corrected type calculation.
16 months ago, by haftmann
some hints on managed installations
16 months ago, by haftmann
prefer cartouches over quotes for clarity of resulting document
16 months ago, by haftmann
A little reorganisation
16 months ago, by paulson
post-release updates;
16 months ago, by wenzelm
merged
16 months ago, by wenzelm
Added tag Isabelle2023 for changeset b5f3d1051b13
16 months ago, by wenzelm
tuned; Isabelle2023
16 months ago, by wenzelm
misc tuning;
16 months ago, by wenzelm
documentation for the "Document" panel in Isabelle/jEdit;
16 months ago, by wenzelm
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
16 months ago, by paulson
merged
16 months ago, by paulson
merged
16 months ago, by paulson
tidying up old apply-style proofs
16 months ago, by paulson
allow higher-order unification of open terms (reviewed by Larry Paulson)
16 months ago, by Kevin Kappelmann
merged
16 months ago, by wenzelm
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
16 months ago, by wenzelm
add ML_system_pp for type Isabelle_Thread.T;
16 months ago, by wenzelm
more explicit type Isabelle_Thread.T;
16 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);
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
tuned Sledgehammer messages
16 months ago, by blanchet
respect timeout better
16 months ago, by blanchet
merged
16 months ago, by wenzelm
Added tag Isabelle2023-RC5 for changeset ffa417b5c913
16 months ago, by wenzelm
tuned;
16 months ago, by wenzelm
tuned messages;
16 months ago, by wenzelm
proper stop of build_process shutdown, despite errors on workers;
16 months ago, by wenzelm
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
16 months ago, by wenzelm
support "isabelle build_worker -q";
16 months ago, by wenzelm
support "isabelle build_process -r -f";
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified output;
16 months ago, by wenzelm
clarified signature;
16 months ago, by wenzelm
clarified signature: removed ununsed option;
16 months ago, by wenzelm
tuned message;
16 months ago, by wenzelm
updated to naproche-20230902: add examples/100_theorems.ftl.tex and some more text in Isabelle/Intro.thy;
16 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;
16 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);
16 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
16 months ago, by wenzelm
more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;
16 months ago, by wenzelm
more accurate documentation of record field update, following changes in Isabelle2007 and Isabelle2008;
16 months ago, by wenzelm
tuned whitespace;
16 months ago, by wenzelm
more robust: "hostname" command might be absent, notably on Arch Linux (and other systemd-based distributions);
16 months ago, by wenzelm
tuned NEWS;
16 months ago, by wenzelm
NEWS;
16 months ago, by wenzelm
update to "scalac -source 3.3" (from 3.1);
16 months ago, by wenzelm
proper pattern (amending ff86f10e54cd);
16 months ago, by wenzelm
discontinue odd AFP partitioning: let Build_Cluster / Build_Engine do the job;
16 months ago, by wenzelm
discontinue special treatment of AFP: "isabelle dump" has been superseded by regular "isabelle build" databases;
16 months ago, by wenzelm
clarified signature: prefer enum types;
16 months ago, by wenzelm