Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
clarified order of modules: early access to interrupt management of Isabelle_Threads;
22 months ago, by wenzelm
tuned: prefer antiquotation for try-catch;
22 months ago, by wenzelm
tuned: prefer antiquotation for try-catch;
22 months ago, by wenzelm
tuned: prefer antiquotation for try-finally;
22 months ago, by wenzelm
omit pointless capture/release (see also 469a375212c1);
22 months ago, by wenzelm
omit pointless capture/release (see also 26774ccb1c74);
22 months ago, by wenzelm
clarified signature: avoid association with potentially dangerous Exn.capture;
22 months ago, by wenzelm
more robust: catch/finally part is uninterruptible;
22 months ago, by wenzelm
more position information, e.g. for warning about fn-pattern;
22 months ago, by wenzelm
unused;
22 months ago, by wenzelm
more general ML_Antiquotation.special_form;
22 months ago, by wenzelm
Importing or moving a few more useful theorems
22 months ago, by paulson
merged
22 months ago, by paulson
A few new theorems
22 months ago, by paulson
avoid legacy binding errors in Sledgehammer Isar proofs
22 months ago, by blanchet
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
22 months ago, by blanchet
added argo
22 months ago, by blanchet
allow (~) syntax in TPTP proofs for unapplied negation
22 months ago, by blanchet
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
22 months ago, by blanchet
use same associativity as Isabelle when parsing HOL proofs
22 months ago, by blanchet
improved Sledgehammer's HOL proof parser w.r.t. negation
22 months ago, by blanchet
clarified signature;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
minor performance tuning;
22 months ago, by wenzelm
merged
22 months ago, by paulson
A few new or simplified proofs
22 months ago, by paulson
tuned: more standard order;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
proper fontenc for cartouches (amending d052d61da398);
22 months ago, by wenzelm
clarified modules;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
clarified modules;
22 months ago, by wenzelm
tuned;
22 months ago, by wenzelm
more robust: prefer linear data flow;
22 months ago, by wenzelm
added first proof reconstruction test for Sledgehammer
22 months ago, by desharna
tuned;
22 months ago, by wenzelm
clarified signature;
22 months ago, by wenzelm
clarified signature (again): follow Isabelle/Java/Scala;
22 months ago, by wenzelm
tuned (following 69c6d3e87660);
22 months ago, by wenzelm
tuned --- avoid pointless indirection (see also a2df9de46060);
22 months ago, by wenzelm
(pointlessly) get rid of some simp calls within "proof"
22 months ago, by paulson
reduced prominence of lemma names
22 months ago, by haftmann
new formulation of an auxiliary lemma
22 months ago, by haftmann
A few more inclusion-exclusion theorems from HOL Light
22 months ago, by paulson
Corrected type calculation.
22 months ago, by haftmann
some hints on managed installations
22 months ago, by haftmann
prefer cartouches over quotes for clarity of resulting document
22 months ago, by haftmann
A little reorganisation
22 months ago, by paulson
post-release updates;
22 months ago, by wenzelm
merged
22 months ago, by wenzelm
Added tag Isabelle2023 for changeset b5f3d1051b13
22 months ago, by wenzelm
tuned;
Isabelle2023
22 months ago, by wenzelm
misc tuning;
22 months ago, by wenzelm
documentation for the "Document" panel in Isabelle/jEdit;
22 months ago, by wenzelm
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
23 months ago, by paulson
merged
23 months ago, by paulson
merged
23 months ago, by paulson
tidying up old apply-style proofs
23 months ago, by paulson
allow higher-order unification of open terms (reviewed by Larry Paulson)
23 months ago, by Kevin Kappelmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
tip