Activity for Archive of Formal Proofs
-
Susannah Mansky committed [d75706]
Updating Jinja from apply-style to Isar-style
-
Susannah Mansky committed [6d1a14]
Merge from default, esp JinjaDCI
-
Susannah Mansky committed [5090fd]
Updating Jinja from apply-style to Isar-style
-
Susannah Mansky committed [ed4bb4]
Updating Jinja from apply-style to Isar-style
-
mraszyk committed [adb5f3]
integrate RBT_Impl optimizations
-
Andreas Lochbihler committed [6de632]
hide MB abbreviation
-
Simon Foster committed [673d65]
Small update to Optics document.
-
Simon Foster committed [0274ab]
Merge
-
wenzelm committed [51acef]
more generous timeout (25min CPU time);
-
wenzelm committed [02a4bc]
non-executable files;
-
wenzelm committed [db241c]
merged
-
Simon Foster committed [fa453a]
Addition of theorems throughout, particularly for prisms.
-
Simon Foster committed [5a13e3]
Added metadata for previous commit (Optics).
-
Gerhard Klein committed [2332e6]
sync with l4v
-
adjustments for Word_Lib updates
-
allow instance for nat
-
Tobias Nipkow committed [f2bc27]
New entry JinjaDCI
-
merge from afp-2020
-
`first` did not have constant time complexity
-
Susannah Mansky committed [944776]
Updating Jinja from apply-style to Isar-style
-
Simon Wimmer committed [c0a61e]
Monad_Memo_DP/Optimal_BST move function argmin
-
Simon Wimmer committed [3d82fe]
Monad_Memo_DP add material on BSTs
-
Simon Wimmer committed [b9ca92]
Cleaning
-
Simon Wimmer committed [78ceb5]
Cleaned
-
Simon Wimmer committed [e69090]
Merged
-
Simon Wimmer committed [bd778b]
Cleaning
-
Simon Wimmer committed [278bc8]
Only one definition of path and weight functions
-
Simon Wimmer committed [e3b9d9]
Improved proof of main correctness theorem for BF
-
Simon Wimmer committed [0eac2d]
Added example and tuned proof
-
Simon Wimmer committed [9cebf8]
Monad_Memo_DP: clean proof, remove unused thms, clean tests
-
Simon Wimmer committed [6c0272]
Fixed guess
-
Simon Wimmer committed [67e783]
Fixed sorries
-
Simon Wimmer committed [b9514d]
Simplified proof
-
Simon Wimmer committed [22a627]
Merged
-
Simon Wimmer committed [cddd9b]
Added bellman-ford implementation with detection of negative cycles
-
Simon Wimmer committed [1190a0]
Make slice abbreviation input only
-
Simon Wimmer committed [3944d6]
Progress on true shortest paths
-
Simon Wimmer committed [1c40d0]
Cycle detection lemma
-
Simon Wimmer committed [8c71fa]
Optimal_BST: simplify termination proofs
-
Simon Wimmer committed [d0819b]
Closed sorries
-
Simon Wimmer committed [c5e379]
Merge updates on dynamic programming
-
Simon Wimmer committed [1171b5]
Finished main theorems on Bellman-Ford
-
Simon Wimmer committed [daebb0]
Tuned proof automation
-
Akihisa Yamada committed [7812e4]
updated description
-
Akihisa Yamada committed [471f6e]
Scott continuity not assuming strictness
-
Akihisa Yamada committed [01c79f]
updating entry for LMCS submission
-
Akihisa Yamada committed [a74436]
forgotten commits
-
Fabian Huch committed [c27ff1]
fix(scala): Updated code for 2.13
-
lp15 committed [016604]
tidied a definition and proof
-
Merge
-
Asta Halkjær From committed [b46909]
Updated comment
-
New entry Hood_Melville_Queue
-
sterraf committed [7f8001]
Adapted to 2021-RC2; renamed lemma ccc_Fn_nat -> ccc_Fn_2
-
sync Word_Lib with l4v
-
more explicit proof
-
merged
-
wenzelm committed [4ee343]
adapted to scala-2.13.4;
-
removed a terrible default simprule
-
Word_Lib: spelling
-
merge from afp-2020
-
Manuel Eberl committed [dd8e0c]
sitegen for CSP_RefTK
-
New (ZF!) entry Delta_System_Lemma
-
webpage for Delta_System_Lemma
-
New submission: CSP_RefTK
-
René Thiemann committed [a80f4e]
sitegen and metadata
-
CSP_RefTK: adjust for Isabelle 1105c42722dc
-
new entry: Topological_Semantics
-
Algebraic_Numbers: some material on algebraic integers
-
wenzelm committed [0d86fc]
isabelle update_cartouches;
-
wenzelm committed [77d672]
tuned -- avoid old-style verbatim text;
-
wenzelm committed [37f216]
merged
-
A bit of tidying
-
cleanup
-
reform
-
moved lemmas such that algebraic numbers theory is not importing factorization algorithm
-
merge
-
proper indentation
-
added code-post lemma for algebraic numbers
-
moved lemmas
-
Julian Brunner committed [5d1dd3]
updated benchmark scripts for iFM paper
-
Julian Brunner committed [d3642b]
fix long-running proof
-
Julian Brunner committed [c1ae04]
merged
-
Peter Gammie committed [5ee969]
Update ConcurrentIMP
-
Update ConcurrentGC
-
adapted to isabelle-dev/74be162a47cd: added some renamings that were missed before
-
adapted to isabelle-dev/74be162a47cd
-
wenzelm committed [824acf]
more standard headers;
-
wenzelm committed [0668d4]
more standard ML file/module names;
-
wenzelm committed [a31f69]
avoid multiple uses of the same ML file;
-
Lars Hupel committed [459344]
Isabelle_Meta_Model: avoid multiple use of ML_file
-
Lars Hupel committed [0327fb]
ensure that at least an empty report file exists
-
Lars Hupel committed [0c0f25]
delete report file if already exists
-
A few tweaks
-
tidying up
-
A little more tidying up
-
more on "summable"
-
wenzelm committed [c541be]
adapted to Isabelle/b1be35908165;
-
wenzelm committed [2bccd7]
clarified defaults: disabled in "isabelle build";
-
wenzelm committed [a34480]
tuned whitespace;
-
wenzelm committed [7684b3]
merged
