![[Jenkins]](/jenkins/static/109fb1e5/images/svgs/logo.svg){kind=logo}
Summary
- merged
- adjust Euler_Polyhedron_Formula to AFP-devel
- merge from AFP 2023
- sitegen
- corrected metadata: doi -> acm identifier
- metadata for Lovasz_Local and Hypergraph_Basics
- new entry: Lovasz_Local
- new entry: Hypergraphs
- metadata and sitegen for Euler Polyhedron Formula
- new entry: Euler's Polyhedron Formula
- adapted to Isabelle/72631efa3821;
- avoid deadly "handle _ => ...";
- tuned: prefer try-catch/finally over low-level 'handle';
- tuned: prefer try-catch/finally over low-level 'handle';
- tuned: prefer try-catch/finally over low-level 'handle';
- clarified signature, following Isabelle/fde0b195cb7d;
- reduced prominence of lemma names
- merge from afp-2023
- regen website
- sync web abstract
- adapted ROOT file link to afp-2023;
- merge from afp-2023
- web: 2023 downlaod links
- Added tag Isabelle2023 for changeset 01bf5fad3e59
- add 2023 release dates
- website regen
- fix toml key generated by afp_releases
- set Isabelle2023 release date
- update Isabelle2022 release dates
- afp release path has changed on isa-afp.org
- fix afp-submit for markdown processing
- Moved a general purpose theorem into the main repository
- a little fix involving the reformulated version of inclusion/exclusion
- fixed missing parenthesis in or-ok-lemma
- new bibiten and titlecase on all sections
- avoid clones of Isabelle/ML operations --- de-emphasize somewhat old/outdated operation;
- replace underscore latex package with formal markup
- merge
- fix latex generation
- Backed out changeset 8eb0a45852dc
- tuned;
- avoid non-local return;
- removed migration tools;
- follow naming conventions of Isabelle/2a99fcb283ee;
- adapted to Isabelle/fd1fec53665b;
- Relational_Disjoint_Set_Forests: update history
- Relational_Disjoint_Set_Forests: minor text edits
- merged
- small fixes
- fix afp-submit for markdown processing
- switch version back to devel after fork
- use default AFP chapter settings
- merge from afp-devel
- update version to 2023
- update author email (by request)
- Tree_Enumeration: Fix errors introduced by renamings in Unidrected_Graph_Theory.
- merge from afp-2022
- sitegen for Fixed_Length_Vector
- added syntax bundles and disabled syntax by default
- moved abstract to root.tex
- made proofs more robust
- new entry Fixed_Length_Vector
- Fixed the title and author of Ceva in the document
- sitegen for Ceva
- new entry Ceva
- for better output notation
- regen website
- fix duplicated key in IEEE_Floating_Point.toml
- Merge changes
- Renamed incident and order to vincident and gorder due to` compatibility issues.
- Note recent additions (roundNearestTiesToAway, single NaN value, SMT-LIB translation) in metadata.
- Merged.
- Registers: Fixed some broken proofs.
- redefine substitution of terms as special case of general evaluation of terms
- Complex_Bounded_Operators: Various changes: - Code generation support for `explicit_cblinfun`. - Various changes and additions in `Cblinfun_Matrix` and `Cblinfun_Code` - Lemma `sandwich_compose`: Switched lhs and rhs. - New lemmas `is_ortho_set_prod`, `ccsubspace_Times_ccspan`. - Definition `cblinfun_inv`: Default value 0 when inverse does not exist. - Renamed `riesz_frechet_representation_...` -> `riesz_representation_...`. - Generalized lemma `inj_ket`.
- update author info
- Update of Combinatorics_Words, Combinatorics_Words_Graph_Lemma, Combinatorics_Words_Lyndon, Two_Generated_Word_Monoids_Intersection, Binary_Code_Imprimitive to to version v1.10.
- metadata formatting
- address metadata warnings
- merge from afp-2022
- remove unused metadata (leaves website unchanged)
- new entry Catoids
- remove obsolete (AFP) group from new entries
- Word_Lib: import new material from l4v
- update to isabelle@fd8e1bbc0686
- merge from afp-2022
- merge from afp-2022
- New entry Polygonal_Number_Theorem
- Quantales_Converse metadata
- new entry Quantales_Converse
- Fixed the punctuation in the title and abstract
- sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser
- New entry /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser
- regenerate site;
- tuned links in theory view;
- tuned instructions;
- regenerate site;
- clarify statistics-ignore flag and build example submission properly;
- regen website
- rectify copy/paste error
- merged
- Redid an ugly proof
- construction for anchord GTT intersection by Alexander Lochman
- merged
- Updated the root file to start from an AFP image
- tuned
- merged
- new editors Lammich and Traytel
- Eliminated needless import and rationalised the ROOT file
- Deleted needless imports
- Generalised and tidied an intermediate result
- Higher_Order_Terms: add fresh_list function
- delete unneeded file
- antiquoting special symbols in text
- merge with default
- Relational_Disjoint_Set_Forests: extended theory, refactored related entries
- Refactored and updated entry. Synchronize with companion paper.
- simplified proof without auxiliary function
- provide more unification algorithms, e.g., to compute mgu's modulo variable renamings
- Adapted to devel
- Relational_Disjoint_Set_Forests: simplified invariant
- Bell_Numbers_Spivey: Add code equations for the computation of Bell numbers.
- Distributed_Distinct_Elements: Swap epsilon/delta for the spec of the algorithm. The reason is to preserve consistency with the upcoming publication to appear at RANDOM 2023.
- proved a few properties of WPO with less assumption, so that Co-WPO properties can be derived
- Fixed LaTeX.
- Merge.
- Fixed missing entries in ROOTS file (previous erronous commit).
- Normalised email.
- Improved setup of the symbolic evaluator.
- Fix proofs broken by previous commit.
- Universal_Hash_Families: Avoid using non-descriptive theory names. Note: The namespace for theory names is global, i.e., a name like "Definitions" is likely to cause collisions.
- merged
- Adjustments for recent cosmetic changes to the Distribution
- Proper epsilon-syntax
- Merge.
- Minor improvement of handling of string literals in symbolic evaluator.
- Removing redundant definitions: - External - Fallback
- tuned
- Merge
- Updating history for Isabelle/Solidity
- Updating Isabelle/Solidity: - Changing expressions do not have side effects anymore. - Adding support for instantiation of contracts. - Adding weakest precondition calculus for the verification of statements.
- Relational_Disjoint_Set_Forests: added a new theory, refactored related entries
- remove some redundant constraint-types in simplex algorithm
- relation between has-maximum and bdd_above
- tuned names
- merged
- more comments
- merged
- back out Paraconsistency
- merged
- tuned and simplified proofs
- Some additions to IICF by Valentin Springsklee
- merge
- small changes in FOL_Seq_Calc1 metadata
- More Paraconsistency
- merged
- tuned
- tuned
- prefer existing Proof_Display.print_theorem (see Isabelle/4dffc47b7e91);
- proper .ML file names;
- proper .ML file name;
- eliminated suspicious Unicode character, which often produce unexpected document output;
- eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91);
- tuned whitespace;
- avoid hardwired document output;
- eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91);
- tuned signature;
- fixed build following a13761ef6796
- merged
- removed unnecessary theory with potential for name conflict
- provided var2-versions of all doubly-nested loops
- Added version of algorithm 4 with precise variant var2 and tuned
- Floyd Warshall: improve code refinements
- IMP2: fix typos
- New check 'coverage_rcv' added.
- Fixing typos.
- Updated formalization to include improvements described in the following publication: Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker. 2023. Stateful Protocol Composition in Isabelle/HOL. ACM Trans. Priv. Secur. 26, 3, Article 25 (August 2023), 36 pages. https://doi.org/10.1145/3577020
- typos
- remove AFP group already defined by chapter;
- Sync with my development repo.