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 Gerhard Klein committed [2332e6]

    sync with l4v

  • Gerhard Klein Gerhard Klein committed [eb0cc2]

    adjustments for Word_Lib updates

  • Gerhard Klein Gerhard Klein committed [6bb5c7]

    allow instance for nat

  • Tobias Nipkow Tobias Nipkow committed [f2bc27]

    New entry JinjaDCI

  • Gerhard Klein Gerhard Klein committed [824ba5]

    merge from afp-2020

  • Tobias Nipkow Tobias Nipkow committed [3c9f87]

    `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 lp15 committed [016604]

    tidied a definition and proof

  • lp15 lp15 committed [4ae553]

    Merge

  • Asta Halkjær From committed [b46909]

    Updated comment

  • Tobias Nipkow Tobias Nipkow committed [bfb558]

    New entry Hood_Melville_Queue

  • sterraf committed [7f8001]

    Adapted to 2021-RC2; renamed lemma ccc_Fn_nat -> ccc_Fn_2

  • Gerhard Klein Gerhard Klein committed [21348d]

    sync Word_Lib with l4v

  • Tobias Nipkow Tobias Nipkow committed [84c055]

    more explicit proof

  • Tobias Nipkow Tobias Nipkow committed [fabc5f]

    merged

  • wenzelm committed [4ee343]

    adapted to scala-2.13.4;

  • lp15 lp15 committed [c7606b]

    removed a terrible default simprule

  • Gerhard Klein Gerhard Klein committed [601908]

    Word_Lib: spelling

  • Gerhard Klein Gerhard Klein committed [f7ada0]

    merge from afp-2020

  • Manuel Eberl Manuel Eberl committed [dd8e0c]

    sitegen for CSP_RefTK

  • lp15 lp15 committed [89ed18]

    New (ZF!) entry Delta_System_Lemma

  • lp15 lp15 committed [2da14e]

    webpage for Delta_System_Lemma

  • Manuel Eberl Manuel Eberl committed [626c95]

    New submission: CSP_RefTK

  • René Thiemann René Thiemann committed [a80f4e]

    sitegen and metadata

  • Gerhard Klein Gerhard Klein committed [52bcf6]

    CSP_RefTK: adjust for Isabelle 1105c42722dc

  • René Thiemann René Thiemann committed [85bc74]

    new entry: Topological_Semantics

  • Manuel Eberl Manuel Eberl committed [03248e]

    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

  • lp15 lp15 committed [7e9db3]

    A bit of tidying

  • René Thiemann René Thiemann committed [1a49a0]

    cleanup

  • René Thiemann René Thiemann committed [29cb25]

    reform

  • René Thiemann René Thiemann committed [7661a1]

    moved lemmas such that algebraic numbers theory is not importing factorization algorithm

  • René Thiemann René Thiemann committed [877ead]

    merge

  • René Thiemann René Thiemann committed [306f9d]

    proper indentation

  • René Thiemann René Thiemann committed [55b144]

    added code-post lemma for algebraic numbers

  • René Thiemann René Thiemann committed [95ca3e]

    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 Peter Gammie committed [5ee969]

    Update ConcurrentIMP

  • Peter Gammie Peter Gammie committed [f972ab]

    Update ConcurrentGC

  • Manuel Eberl Manuel Eberl committed [8bf81d]

    adapted to isabelle-dev/74be162a47cd: added some renamings that were missed before

  • Manuel Eberl Manuel Eberl committed [dfe83c]

    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

  • lp15 lp15 committed [7b26d4]

    A few tweaks

  • lp15 lp15 committed [99c2ec]

    tidying up

  • lp15 lp15 committed [222edc]

    A little more tidying up

  • lp15 lp15 committed [1e5355]

    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

1 >