Summary
- merged
- sitegen for Continued_Fractions
- New entry "Continued_Fractions"
- sitegen for Approximate_Model_Counting
- tuned (removing warnings)
- new entry Approximate_Model_Counting
- Go: website updates
- Go submission
- adapt to Isabelle/11a1f4d7af51;
- use emph instead of italic;
- tuned;
- clarified names;
- tuned lemmas
- merged
- removed stuff moved to the Isabelle distribution
- avoid java.net.URL, following Isabelle/a4118f530263;
- updated: standard Borel
- use time_fun command
- merged
- Splay tree analysis now uses time_fun command
- tuned proofs to reduce verification time following Isabelle/7735645667f0
- merge
- feat(Transport) major improvement of overloaded properties + new relational properties
- fix(ML_Unification) replace binders before aeconv (avoids lowering)
- feat(ML_Unification) add simplification+unification unifier; fix context merge bug for uhints; cleaner code
- merged
- adapted to new definition of wf following Isabelle/033f90dc441d
- merged
- Two new lemmas by Eberl (requested by Paulson)
- adapted to isabelle/devel
- adapted to new definition of wfP following Isabelle/233d70cad0cf
- updated url
- merged
- tuned proof
- Patching some proofs, for of_nat_int_ceiling
- Deletion of material that had been moved to the distribution
- Multirelations_Heterogeneous: further results for convex-closure
- added some material about the Laurent expansion of zeta
- Remove stuff following Isabelle/d0205dde00bb and related changesets
- fixed broken definitions and proofs following Isabelle/8d153846f65f
- Universal_Hash_Families: Remove accidental duplication of pmf_of_set_prod_eq.
- Inserted a corollary to the main result
- Updated a proof to the new formalisation of meromorphic
- Relational_Cardinality: minor revision
- adapted to Isabelle/2746dfc9ceae;
- merge
- adjusting HOL-CSP_OpSem from 2023 to devel
- merge from AFP 2023
- metadata for HOL-CSP OpSem and sitegen
- new entry: HOL-CSP OpSem
- removed lemmas following Isabelle/ba8fb71587ae
- merge from AFP 2023
- sitegen for Wieferich Kempner
- new entry: Wieferich Kempner
- merge from AFP 2023
- metadata and sitegen for QBF-Solver
- new entry: QBF_Solver_Verification
- further files for CubicalCategories
- New entry CubicalCategories
- update doc;
- Correction of an error in the abstract
- sitegen for Karatsuba
- New submission: Karatsuba
- adjusted proof
- more accurate timeout; tuned whitespace;
- move multiset lemmas into distro
- non-executable files;
- Moving library material into Analysis (Elementary_Metric_Spaces and Set_Integration)
- New version consistent with paper
- tuned proof: avoid z3 to make it work on arm64-linux;
- tuned proof: avoid z3 to make it work on arm64-linux;
- tuned proof: avoid z3 to make it work on arm64-linux;
- tuned proof: avoid z3 to make it work on arm64-linux;
- tuned whitespace;
- tuned proof: avoid z3 to make it work on arm64-linux;
- tuned whitespace;
- backed out changeset ddf90847bfa5: still requires approx. 8-10h elapsed time / 50h CPU time on common test hardware (see 13b3e24a71b0), only latest x86_64-linux hardware is reasonably fast (3.5h elapsed time, 20h CPU time seen on of1.proof.cit.tum.de), but arm64-darwin is very slow;
- tuned signature, following Isabelle/da4e82434985;
- adapted to Isabelle/3648e9c88d0c;
- Fixed a rewriting issue
- Resolved a syntax clash involving Equipollence (now imported by Ramsey)
- enable proof in session Lorenz_C1
- simplified proofs
- simplified proof
- Incorporating library material from AFP sessions
- avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic
- merged
- Removed numerous z3 calls and tried to simplify some extremely messy proofs
- Adjustments for recent changes to the main repository
- A little tidying up. Removed some smt calls
- avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic
- tuned proofs
- Simpl: remove stray thm command
- CRYSTALS-Kyber_Security: adapt to isabelle@cff4576218fa
- Interval_Analysis: adapt to isabelle@cff4576218fa
- merge from afp-2023
- update Simpl entry; change license to BSD (submission by Norbert Schirmer)
- sitegen for IMP_Noninterference
- New entry IMP_Noninterference
- sitegen for Sumcheck Protocol
- new entry Sumcheck Protocol
- New entry OmegaCatoidsQuantales
- New submission Region_Quadtrees
- sitegen and metadata for Isabelle_hoops
- New entry Isabelle_hoops (with its name standardised)
- sitegen and metadata for Interval_Analysis
- New submission Interval_Analysis
- New entry CRYSTALS-Kyber_Security
- proper Homepage comparison: URL equals does not fulfil specification;
- A lot of tidying
- merged
- Tidied up some messy proofs
- Cleaning and simplifying notation
- A little tidying. Removal of z3 smt calls
- formally normalized definition of singleton shifts to their primitive form
- Integration syntax
- Importation of the infinite type class
- the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
- Moving a few facts from libraries into the main repository
- Shortening some proofs
- Correcting misleading notation
- simplified class specification
- more realistic timeouts;
- Borrowed prod_mono_strict' for the distribution; adjusted proofs
- merged
- added lifting of forward simulation to transitive closure
- Renamed a theorem involving convexity
- Updated a proof for the corrected version of convex_on
- Made the proof slightly more explicit
- Fixed a problem involving sum_diff_split
- New lemmas and renaming of lemmas
- feat(ML_Unification,Transport) more robust unification + new unifiers
- strengthened class parity
- "Moving up" AFP library material to more appropriate places
- merged
- Simplification of some of the lemma libraries
- merged
- use define_time_function
- common type class for trivial properties on div/mod
- Expander_Graphs: Add additional tail bound for expander random walks.
- rearranged and reformulated abstract classes for bit structures and operations
- Universal_Hash_Families and Expander_Graphs: Framework for pseudorandom objects Pseudorandom objects as a combinator library was formerly incorrectly part of the Distribtued_Distinct_Elements AFP entry due to chronological reasons. But it belongs conceptually to the Universal_Hash_Families and Expander_Graphs entries, which this patch accomplishes. Compared to the former development in DDE the new framework also includes several improvements: - Constructive implementation of hash families - An object is always non-empty - this means every object induces naturally a PMF, which removes a lot of constraints from the theorems. Note: The theory DDE/Pseudorandom_Combinators is now obsolete. I will remove it shortly before the next release (to minimize the possibility of merge-conflicts).
- tuned signature;
- adapted to Isabelle/c7a98469c0e7;
- Frequency_Moments and Expander_Graphs: Change the dependency between the entries. The dependency of Expander_Graphs to Frequency_Moments was due to the use of some auxiliary results (in particular those about HOL-Probability.Product_PMF). This change moves those to Universal_Hash_Families, so that the dependency can be avoided. Note: I added aliases and abbreviations to minimize the risk of merge-conflicts. This change will enable the introduction of further additional examples, that show how Expander Graphs can be used to further improve the space complexity of the verified algorithms in Frequency_Moments.
- merge
- feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex instantiations
- Universal_Hash_Families: Remove duplicate proofs (caused by previous commit.)
- Finite_Fields: Add exectuable algorithms for the construction of (and calculation in) finite fields.
- Finite Fields: Minor improvements to previous commit.
- Finite_Fields: Add Rabin's test for the irreducibility of polynomials.
- Finite Fields: Add more general lower estimate for cardinality of irreducible polynomials.
- Distributed_Distinct_Elements: Add related entries.
- Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities.
- Renamed a theorem
- streamlined type class specification
- consolidated lemma name
- simplified specification of type class
- consolidated name of lemma analogously to nat/int/word_bit_induct
- tuned finite proofs
- merged
- adapted to Isabelle/7d10708bbc32;
- adapted to isabelle/devel
- Relational_Disjoint_Set_Forests: minor revision
- more realistic timeout;
- fix(ML_Unification) use cartouches to fix document build error
- feat(ML_Unification) more explanation
- merge
- feat(Transport) better relativised concept definitions and lemmas
- feat(ML_Unification) add recursive unification hints fallback option
- CZH_Foundations: integration with Cardinality_Continuum
- tuned;
- tuned;
- adapted to Isabelle/e1895596e1b9;
- adapted to Isabelle/c6c2e41cac1c;
- proper terminology;
- removed outdated comments;
- adapted to Isabelle/70c0dbfacf0b;
- tuned;
- tuned, following Isabelle/8c9cce335a3d;
- tuned;
- tuned;
- tuned;
- tuned;
- tuned;
- tuned, following Isabelle/e7796c55d840;
- Hello_World: add some descriptive text
- Introduced definition for the sigma algebra at infinity for a filtration.
- Fixed issue that caused Martingales to not compile. Sorry!
- re-introduce code in session of Hello_World
- adapted to Isabelle/032a31db4c6f;
- adjusted HOL-CSPM from 2023 to development (Patch.thy might need further cleanup)
- Updated entry Martingales.
- adapted Disintegration to devel
- adapted to isabelle-dev;
- adjusted Concentration Inequalities from 2023 to devel
- merge from AFP 2023
- tuned
- New entry KnuthMorrisPratt
- metadata and sitegen
- new entry: HOL-CSPM
- sitegen for Martingales
- new entry Martingales
- sitegen for Concentration_Inequalities
- new entry Concentration_Inequalities
- New entry: Lambert_Series
- adjusted doi capitalization
- sitegen for Q0_soundness
- new entry Q0_Soundness
- sitegen for Cardinality_Continuum
- new entry Cardinality_Continuum
- Polylog web files
- sitegen for Polylog
- New entry: Polylog
- sitegen for Polynomial_Crit_Geometry
- new entry Polynomial_Crit_Geometry
- sitegen for Chebyshev_Polynomials
- New entry Chebyshev_Polynomials
- more website for LTL and PD
- website for LTL and PD
- Labeled_Transition_Systems and Pushdown_Systems
- New entry: Nominal_Myhill_Nerode
- more doc;
- sitegen for Q0_Metatheory
- updated LaTeX citations
- new entry Q0_Metatheory
- Perfect_Fields and Elimination_Of_Repeated_Factors incl sitegen
- New entry Perfect_Fields
- sitegen for /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Disintegration
- New entry "Disintegration"
- allow partially detecting potential name conflicts;
- added check to detect potential name conflicts;
- add warning for missing DOI cache;
- Eudoxus_Reals patch and sitegen
- New entry, Eudoxus_Reals
- New entry /Hypergraph_Colourings
- adapted to Isabelle/99bc2dd45111;
- adapted to simplified T convention
- merged
- adapted to new T conventions
- extracted lemma finite_progress out of proof
- simplified proof
- merged
- tuned lift_strong_simulation_to_bisimulation
- simplified definition of match_bisim
- strengthened lift_strong_simulation_to_bisimulation and simplified match_bisim
- adadpted to [simp] changes in distrib
- de-duplicated specification of class ring_bit_operations
- adjusted T_sift_down: all primitives take 0 time.
- added missing file following 2702f2046afa
- documented change in VeriComp
- added framework-independent lemma to lift simulation to bisimulation
- tuned
- added publication
- slightly more elementary characterization of unset_bit
- base abstract specification of NOT on recursive equation rather than bit projection
- more realistic timeouts for lrzcloud2:threads=1;
- tuned proof
- more realistic timeouts for lrzcloud2:threads=1;
- operations AND, OR, XOR are specified by characteristic recursive equation
- some extensions to Cotangent_PFD_Formula
- slightly less technical formulation of very specific type class