Changes
#35 (Apr 2, 2024, 1:42:25 PM)
- make Go test mandatory — Lars Hupel <lars@hupel.info> / hgweb
- remove generated files — Lars Hupel <lars@hupel.info> / hgweb
- remove "horrible workaround", fixed in upstream Isabelle (authored by Terru) — Lars Hupel <lars@hupel.info> / hgweb
- adapted Zeta_3_Irrational w.r.t. isabelle/4c1347e172b1 — Manuel Eberl <eberlm@in.tum.de> / hgweb
- adapted to isabelle/4c1347e172b1 — Manuel Eberl <eberlm@in.tum.de> / hgweb
- moved web_app to distribution (see Isabelle/37ea0727291f); — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified web app parameters; — Fabian Huch <huch@in.tum.de> / hgweb
- proper topic input validation; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified web_app paths: better naming, more operations; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp_submit: moved submission logic to model; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp_submit: separate model, view, and (API) paths properly; — Fabian Huch <huch@in.tum.de> / hgweb
- better rendering of submission archive and Isabelle log; — Fabian Huch <huch@in.tum.de> / hgweb
- proper state handling in submission handler; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned name; — Fabian Huch <huch@in.tum.de> / hgweb
- add explicit synchronized server state; — Fabian Huch <huch@in.tum.de> / hgweb
- more uniform load_entries; — Fabian Huch <huch@in.tum.de> / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- tuned: prefer for-comprehension in complicated situations; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned formatting; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned: more uniform Isabelle style; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned imports; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified options; — Fabian Huch <huch@in.tum.de> / hgweb
- Distributed_Distinct_Elements: Fix aliasing issue introduce in isabelle distribution. — Emin Karayel <me@eminkarayel.de> / hgweb
- merged — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- clarified types: richer interface for metadata; — Fabian Huch <huch@in.tum.de> / hgweb
- add option to run formatting operations on all metadata files; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- update to Isabelle/42bc8ab751c1; — wenzelm / hgweb
- proper Go setup, following Isabelle/da323d3d7570; — wenzelm / hgweb
#34 (Mar 27, 2024, 10:09:14 PM)
- proper Go setup, following Isabelle/1e7d4372fe3d; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proofs: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- updates to new time function generator that now translates undefined to undefined, not 0 — nipkow / hgweb
- Fixes mostly for log_mono aliasing — paulson <lp15@cam.ac.uk> / hgweb
- Brought this new entry up-to-date with the development version — paulson <lp15@cam.ac.uk> / hgweb
#33 (Mar 26, 2024, 9:21:19 PM)
- merged — Lars Hupel <lars@hupel.info> / hgweb
- sitegen for Continued_Fractions — paulson <lp15@cam.ac.uk> / hgweb
- New entry "Continued_Fractions" — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Approximate_Model_Counting — traytel / hgweb
- tuned (removing warnings) — traytel / hgweb
- new entry Approximate_Model_Counting — traytel / hgweb
- Go: website updates — Peter Lammich / hgweb
- Go submission — Peter Lammich / hgweb
- adapt to Isabelle/11a1f4d7af51; — Fabian Huch <huch@in.tum.de> / hgweb
- use emph instead of italic; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified names; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned lemmas — desharna / hgweb
- merged — desharna / hgweb
- removed stuff moved to the Isabelle distribution — desharna / hgweb
- avoid java.net.URL, following Isabelle/a4118f530263; — Fabian Huch <huch@in.tum.de> / hgweb
- updated: standard Borel — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
- use time_fun command — nipkow / hgweb
- merged — nipkow / hgweb
- Splay tree analysis now uses time_fun command — nipkow / hgweb
- tuned proofs to reduce verification time following Isabelle/7735645667f0 — desharna / hgweb
- merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- feat(Transport) major improvement of overloaded properties + new relational properties — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- fix(ML_Unification) replace binders before aeconv (avoids lowering) — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- feat(ML_Unification) add simplification+unification unifier; fix context merge bug for uhints; cleaner code — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merged — desharna / hgweb
- adapted to new definition of wf following Isabelle/033f90dc441d — desharna / hgweb
- merged — paulson / hgweb
- Two new lemmas by Eberl (requested by Paulson) — paulson <lp15@cam.ac.uk> / hgweb
- adapted to isabelle/devel — nipkow / hgweb
- adapted to new definition of wfP following Isabelle/233d70cad0cf — desharna / hgweb
- updated url — nipkow / hgweb
- merged — desharna / hgweb
- tuned proof — desharna / hgweb
- Patching some proofs, for of_nat_int_ceiling — paulson <lp15@cam.ac.uk> / hgweb
- Deletion of material that had been moved to the distribution — paulson <lp15@cam.ac.uk> / hgweb
- Multirelations_Heterogeneous: further results for convex-closure — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- added some material about the Laurent expansion of zeta — Manuel Eberl <manuel@pruvisto.org> / hgweb
- Remove stuff following Isabelle/d0205dde00bb and related changesets — desharna / hgweb
- fixed broken definitions and proofs following Isabelle/8d153846f65f — desharna / hgweb
- Universal_Hash_Families: Remove accidental duplication of pmf_of_set_prod_eq. — Emin Karayel <me@eminkarayel.de> / hgweb
- Inserted a corollary to the main result — paulson <lp15@cam.ac.uk> / hgweb
- Updated a proof to the new formalisation of meromorphic — paulson <lp15@cam.ac.uk> / hgweb
- Relational_Cardinality: minor revision — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- adapted to Isabelle/2746dfc9ceae; — wenzelm / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusting HOL-CSP_OpSem from 2023 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for HOL-CSP OpSem and sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: HOL-CSP OpSem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- removed lemmas following Isabelle/ba8fb71587ae — desharna / hgweb
- merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Wieferich Kempner — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Wieferich Kempner — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata and sitegen for QBF-Solver — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: QBF_Solver_Verification — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- further files for CubicalCategories — nipkow / hgweb
- New entry CubicalCategories — nipkow / hgweb
- update doc; — Fabian Huch <huch@in.tum.de> / hgweb
- Correction of an error in the abstract — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Karatsuba — paulson <lp15@cam.ac.uk> / hgweb
- New submission: Karatsuba — paulson <lp15@cam.ac.uk> / hgweb
- adjusted proof — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- more accurate timeout;
tuned whitespace; — wenzelm / hgweb - move multiset lemmas into distro — blanchet / hgweb
- non-executable files; — wenzelm / hgweb
- Moving library material into Analysis (Elementary_Metric_Spaces and Set_Integration) — paulson <lp15@cam.ac.uk> / hgweb
- New version consistent with paper — nipkow / hgweb
- tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- 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; — wenzelm / hgweb
- tuned signature, following Isabelle/da4e82434985; — wenzelm / hgweb
- adapted to Isabelle/3648e9c88d0c; — Fabian Huch <huch@in.tum.de> / hgweb
- Fixed a rewriting issue — paulson <lp15@cam.ac.uk> / hgweb
- Resolved a syntax clash involving Equipollence (now imported by Ramsey) — paulson <lp15@cam.ac.uk> / hgweb
- enable proof in session Lorenz_C1 — immler / hgweb
- simplified proofs — blanchet / hgweb
- simplified proof — blanchet / hgweb
- Incorporating library material from AFP sessions — paulson <lp15@cam.ac.uk> / hgweb
- avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic — blanchet / hgweb
- merged — paulson / hgweb
- Removed numerous z3 calls and tried to simplify some extremely messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- Adjustments for recent changes to the main repository — paulson <lp15@cam.ac.uk> / hgweb
- A little tidying up. Removed some smt calls — paulson <lp15@cam.ac.uk> / hgweb
- avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic — blanchet / hgweb
- tuned proofs — blanchet / hgweb
- Simpl: remove stray thm command — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- CRYSTALS-Kyber_Security: adapt to isabelle@cff4576218fa — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Interval_Analysis: adapt to isabelle@cff4576218fa — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update Simpl entry; change license to BSD
(submission by Norbert Schirmer) — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb - sitegen for IMP_Noninterference — paulson <lp15@cam.ac.uk> / hgweb
- New entry IMP_Noninterference — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Sumcheck Protocol — traytel / hgweb
- new entry Sumcheck Protocol — traytel / hgweb
- New entry OmegaCatoidsQuantales — nipkow / hgweb
- New submission Region_Quadtrees — paulson <lp15@cam.ac.uk> / hgweb
- sitegen and metadata for Isabelle_hoops — paulson <lp15@cam.ac.uk> / hgweb
- New entry Isabelle_hoops (with its name standardised) — paulson <lp15@cam.ac.uk> / hgweb
- sitegen and metadata for Interval_Analysis — paulson <lp15@cam.ac.uk> / hgweb
- New submission Interval_Analysis — paulson <lp15@cam.ac.uk> / hgweb
- New entry CRYSTALS-Kyber_Security — nipkow / hgweb
- proper Homepage comparison: URL equals does not fulfil specification; — Fabian Huch <huch@in.tum.de> / hgweb
- A lot of tidying — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Tidied up some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- Cleaning and simplifying notation — carolos@live.nl / hgweb
- A little tidying. Removal of z3 smt calls — paulson <lp15@cam.ac.uk> / hgweb
- formally normalized definition of singleton shifts to their primitive form — haftmann / hgweb
- Integration syntax — paulson <lp15@cam.ac.uk> / hgweb
- Importation of the infinite type class — paulson <lp15@cam.ac.uk> / hgweb
- the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses — paulson <lp15@cam.ac.uk> / hgweb
- Moving a few facts from libraries into the main repository — paulson <lp15@cam.ac.uk> / hgweb
- Shortening some proofs — carolos@live.nl / hgweb
- Correcting misleading notation — carolos@live.nl / hgweb
- simplified class specification — haftmann / hgweb
- more realistic timeouts; — wenzelm / hgweb
- Borrowed prod_mono_strict' for the distribution; adjusted proofs — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- added lifting of forward simulation to transitive closure — desharna / hgweb
- Renamed a theorem involving convexity — paulson <lp15@cam.ac.uk> / hgweb
- Updated a proof for the corrected version of convex_on — paulson <lp15@cam.ac.uk> / hgweb
- Made the proof slightly more explicit — paulson <lp15@cam.ac.uk> / hgweb
- Fixed a problem involving sum_diff_split — paulson <lp15@cam.ac.uk> / hgweb
- New lemmas and renaming of lemmas — paulson <lp15@cam.ac.uk> / hgweb
- feat(ML_Unification,Transport) more robust unification + new unifiers — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- strengthened class parity — haftmann / hgweb
- "Moving up" AFP library material to more appropriate places — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Simplification of some of the lemma libraries — paulson <lp15@cam.ac.uk> / hgweb
- merged — nipkow / hgweb
- use define_time_function — nipkow / hgweb
- common type class for trivial properties on div/mod — haftmann / hgweb
- Expander_Graphs: Add additional tail bound for expander random walks. — Emin Karayel <me@eminkarayel.de> / hgweb
- rearranged and reformulated abstract classes for bit structures and operations — haftmann / hgweb
- 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). — Emin Karayel <me@eminkarayel.de> / hgweb - tuned signature; — wenzelm / hgweb
- adapted to Isabelle/c7a98469c0e7; — wenzelm / hgweb
- 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. — Emin Karayel <me@eminkarayel.de> / hgweb - merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- feat(ML_Unification) fix exceptions and improve experience wrt. flex-flex instantiations — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- Universal_Hash_Families: Remove duplicate proofs (caused by previous commit.) — Emin Karayel <me@eminkarayel.de> / hgweb
- Finite_Fields: Add exectuable algorithms for the construction of (and calculation in) finite fields. — Emin Karayel <me@eminkarayel.de> / hgweb
- Finite Fields: Minor improvements to previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
- Finite_Fields: Add Rabin's test for the irreducibility of polynomials. — Emin Karayel <me@eminkarayel.de> / hgweb
- Finite Fields: Add more general lower estimate for cardinality of irreducible polynomials. — Emin Karayel <me@eminkarayel.de> / hgweb
- Distributed_Distinct_Elements: Add related entries. — Emin Karayel <me@eminkarayel.de> / hgweb
- Frequency_Moments: Remove duplication of lemmas from Concentration_Inequalities. — Emin Karayel <me@eminkarayel.de> / hgweb
- Renamed a theorem — paulson <lp15@cam.ac.uk> / hgweb
- streamlined type class specification — haftmann / hgweb
- consolidated lemma name — haftmann / hgweb
- simplified specification of type class — haftmann / hgweb
- consolidated name of lemma analogously to nat/int/word_bit_induct — haftmann / hgweb
- tuned finite proofs — nipkow / hgweb
- merged — wenzelm / hgweb
- adapted to Isabelle/7d10708bbc32; — wenzelm / hgweb
- adapted to isabelle/devel — nipkow / hgweb
- Relational_Disjoint_Set_Forests: minor revision — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- more realistic timeout; — wenzelm / hgweb
- fix(ML_Unification) use cartouches to fix document build error — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- feat(ML_Unification) more explanation — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- feat(Transport) better relativised concept definitions and lemmas — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- feat(ML_Unification) add recursive unification hints fallback option — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- CZH_Foundations: integration with Cardinality_Continuum — user9716869 <user9716869@gmail.com> / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- adapted to Isabelle/e1895596e1b9; — wenzelm / hgweb
- adapted to Isabelle/c6c2e41cac1c; — wenzelm / hgweb
- proper terminology; — wenzelm / hgweb
- removed outdated comments; — wenzelm / hgweb
- adapted to Isabelle/70c0dbfacf0b; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned, following Isabelle/8c9cce335a3d; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned, following Isabelle/e7796c55d840; — wenzelm / hgweb
- Hello_World: add some descriptive text — Lars Hupel <lars@hupel.info> / hgweb
- Introduced definition for the sigma algebra at infinity for a filtration. — Ata Keskin <ata.keskin@tum.de> / hgweb
- Fixed issue that caused Martingales to not compile. Sorry! — Ata Keskin <ata.keskin@tum.de> / hgweb
- re-introduce code in session of Hello_World — Lars Hupel <lars@hupel.info> / hgweb
- adapted to Isabelle/032a31db4c6f; — wenzelm / hgweb
- adjusted HOL-CSPM from 2023 to development (Patch.thy might need further cleanup) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Updated entry Martingales. — Ata Keskin <ata.keskin@tum.de> / hgweb
- adapted Disintegration to devel — Manuel Eberl <eberlm@in.tum.de> / hgweb
- adapted to isabelle-dev; — wenzelm / hgweb
- adjusted Concentration Inequalities from 2023 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned — nipkow / hgweb
- New entry KnuthMorrisPratt — nipkow / hgweb
- metadata and sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: HOL-CSPM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Martingales — Manuel Eberl <eberlm@in.tum.de> / hgweb
- new entry Martingales — Manuel Eberl <eberlm@in.tum.de> / hgweb
- sitegen for Concentration_Inequalities — Manuel Eberl <eberlm@in.tum.de> / hgweb
- new entry Concentration_Inequalities — Manuel Eberl <eberlm@in.tum.de> / hgweb
- New entry: Lambert_Series — nipkow / hgweb
- adjusted doi capitalization — traytel / hgweb
- sitegen for Q0_soundness — traytel / hgweb
- new entry Q0_Soundness — traytel / hgweb
- sitegen for Cardinality_Continuum — traytel / hgweb
- new entry Cardinality_Continuum — traytel / hgweb
- Polylog web files — nipkow / hgweb
- sitegen for Polylog — nipkow / hgweb
- New entry: Polylog — nipkow / hgweb
- sitegen for Polynomial_Crit_Geometry — paulson <lp15@cam.ac.uk> / hgweb
- new entry Polynomial_Crit_Geometry — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Chebyshev_Polynomials — paulson <lp15@cam.ac.uk> / hgweb
- New entry Chebyshev_Polynomials — paulson <lp15@cam.ac.uk> / hgweb
- more website for LTL and PD — lammich <lammich@in.tum.de> / hgweb
- website for LTL and PD — lammich <lammich@in.tum.de> / hgweb
- Labeled_Transition_Systems and Pushdown_Systems — lammich <lammich@in.tum.de> / hgweb
- New entry: Nominal_Myhill_Nerode — nipkow / hgweb
- more doc; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen for Q0_Metatheory — traytel / hgweb
- updated LaTeX citations — traytel / hgweb
- new entry Q0_Metatheory — traytel / hgweb
- Perfect_Fields and Elimination_Of_Repeated_Factors incl sitegen — paulson <lp15@cam.ac.uk> / hgweb
- New entry Perfect_Fields — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Disintegration — paulson <lp15@cam.ac.uk> / hgweb
- New entry "Disintegration" — paulson <lp15@cam.ac.uk> / hgweb
- allow partially detecting potential name conflicts; — Fabian Huch <huch@in.tum.de> / hgweb
- added check to detect potential name conflicts; — Fabian Huch <huch@in.tum.de> / hgweb
- add warning for missing DOI cache; — Fabian Huch <huch@in.tum.de> / hgweb
- Eudoxus_Reals patch and sitegen — paulson <lp15@cam.ac.uk> / hgweb
- New entry, Eudoxus_Reals — paulson <lp15@cam.ac.uk> / hgweb
- New entry /Hypergraph_Colourings — nipkow / hgweb
- adapted to Isabelle/99bc2dd45111; — wenzelm / hgweb
- adapted to simplified T convention — nipkow / hgweb
- merged — nipkow / hgweb
- adapted to new T conventions — nipkow / hgweb
- extracted lemma finite_progress out of proof — desharna / hgweb
- simplified proof — nipkow / hgweb
- merged — desharna / hgweb
- tuned lift_strong_simulation_to_bisimulation — desharna / hgweb
- simplified definition of match_bisim — desharna / hgweb
- strengthened lift_strong_simulation_to_bisimulation and simplified match_bisim — desharna / hgweb
- adadpted to [simp] changes in distrib — nipkow / hgweb
- de-duplicated specification of class ring_bit_operations — haftmann / hgweb
- adjusted T_sift_down: all primitives take 0 time. — nipkow / hgweb
- added missing file following 2702f2046afa — desharna / hgweb
- documented change in VeriComp — desharna / hgweb
- added framework-independent lemma to lift simulation to bisimulation — desharna / hgweb
- tuned — nipkow / hgweb
- added publication — nipkow / hgweb
- slightly more elementary characterization of unset_bit — haftmann / hgweb
- base abstract specification of NOT on recursive equation rather than bit projection — haftmann / hgweb
- more realistic timeouts for lrzcloud2:threads=1; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned proof — haftmann / hgweb
- more realistic timeouts for lrzcloud2:threads=1; — wenzelm / hgweb
- operations AND, OR, XOR are specified by characteristic recursive equation — haftmann / hgweb
- some extensions to Cotangent_PFD_Formula — Manuel Eberl <manuel@pruvisto.org> / hgweb
- slightly less technical formulation of very specific type class — haftmann / hgweb
#32 (Nov 6, 2023, 7:33:09 PM)
- fixed duplicate theory name in Polynomial_Factorization — Manuel Eberl <eberlm@in.tum.de> / hgweb
- refactored proof — traytel / hgweb
- merged — paulson / hgweb
- Removal of the original and obsolete development; replaced by links to the corresponding theorems in the Isabelle libraries — paulson <lp15@cam.ac.uk> / hgweb
- more realistic timeout; — wenzelm / hgweb
- proper document setup for \usepackage{times};
drop extra copy of generated document; — wenzelm / hgweb - more realistic timeout; — wenzelm / hgweb
- avoid hardwired document output; — wenzelm / hgweb
- merge — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- fix(ML_Unification/Parsing) change map_safe type to return an option — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- Fixed issues connected with cong_def vs unique_euclidean_semiring_class.cong_def and := syntax — paulson <lp15@cam.ac.uk> / hgweb
- Got rid of some global (and unnecessary) parameter settings. Also fixed a couple of slow proofs — paulson <lp15@cam.ac.uk> / hgweb
- feat(ML_Unification) use fixed parser from Isabelle distro — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merged — desharna / hgweb
- removed unnecessary condition that decided literals are in N — desharna / hgweb
- added name to corollary — desharna / hgweb
- removed lemma now in distribution — desharna / hgweb
- added lemma right_unique_skip — desharna / hgweb
- Stone_Relation_Algebras: minor additions — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- merged — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
- Standard_Borel_Spaces: removed an unnecessary file — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
- Standard_Borel_Spaces and S_Finite_Measure_Monad: adjust theories to metric space in Isabelle2023 — Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> / hgweb
- remove ci-extras component (see Isabelle/f992769d); — Fabian Huch <huch@in.tum.de> / hgweb
- use ci build mail server; — Fabian Huch <huch@in.tum.de> / hgweb
- use Isabelle options for CI mail settings (see Isabelle/4c5aadf1); — Fabian Huch <huch@in.tum.de> / hgweb
- removed unused/broken clone (see Isabelle/aff231884b20); — wenzelm / hgweb
- adaptred to Isabelle/d769a183d51d; — wenzelm / hgweb
- more standard simproc_setup using ML antiquotation; — wenzelm / hgweb
- adapted to Isabelle/807b249f1061; — wenzelm / hgweb
- clarified simproc_setup (passive); — wenzelm / hgweb
- avoid clash with outer syntax keyword 'passive'; — wenzelm / hgweb
- merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Transport sitegen — paulson <lp15@cam.ac.uk> / hgweb
- New submission Transport — paulson <lp15@cam.ac.uk> / hgweb
- update S_Finite_Measure_Monad to Isabelle2023 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- web pages for Standard_Borel_Spaces and S_Finite_Measure_Monad — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- update Standard_Borel_Spaces to Isabelle2023 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- theory files for S_Finite_Measure_Monad + Standard_Borel_Spaces — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- new entry IO_Language_Conformance — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- new entry Coupledsim_Contrasim — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- drop SN from standard wpo-assumptions; prove irreflexivity of WPO without SN — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added proof: the multiset extension of two orders preserves irreflexivity — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added lemmas on lexicographic extension — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added code-unfold lemma — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- fix(ML_Unification) remove temporary files — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- update hugo to 0.119.0; — Fabian Huch <huch@in.tum.de> / hgweb
- moved hugo component build tool to Isabelle distribution; — Fabian Huch <huch@in.tum.de> / hgweb
- update hugo component and support more platforms; — Fabian Huch <huch@in.tum.de> / hgweb
#31 (Oct 6, 2023, 9:33:16 AM)
- merge from afp-2023; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- change web path to /sessions/ instead of /theories/ for consistent naming scheme; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned: remove hugo warnings; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned whitespace; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- display only unique exact matches in topic listing; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- remove automatic title capitalization; — Fabian Huch <huch@in.tum.de> / hgweb
- improve description of the submission process; — Fabian Huch <huch@in.tum.de> / hgweb
- improved path resolving in theory view; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- generate theory listings for dependencies in distribution; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- obtain theory html file urls from browser_info instead of hard-coded links; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned whitespace; — Fabian Huch <huch@in.tum.de> / hgweb
- record proper entry dependencies instead of relying on coincidental session names; — Fabian Huch <huch@in.tum.de> / hgweb
- clarify chapter urls: remove from config as they are a separate concept; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen — traytel / hgweb
- new entry ML_Unification — traytel / hgweb
- Inserted another missing acknowledgement — paulson <lp15@cam.ac.uk> / hgweb
- fix web; — Fabian Huch <huch@in.tum.de> / hgweb
- added missing files — nipkow / hgweb
- New entry Relational_Cardinality — nipkow / hgweb
- Acknowledging the Alexandria project in two entries — paulson <lp15@cam.ac.uk> / hgweb
- Adaption to new HOL-CSP core; some stronger compactification theorems. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Integrated many contributions by Benoit Ballenghuin.
- shorter proofs in CSP
- theory CSP_Induct
- theory Renaming
- updates on documentation — Burkhart Wolff <wolff@lri.fr> / hgweb - merged — nipkow / hgweb
- more lit.refs — nipkow / hgweb
- Removal of material that had already been migrated to the repository — paulson <lp15@cam.ac.uk> / hgweb
- added lit.ref. — nipkow / hgweb
- sitegen — nipkow / hgweb
- fix link; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen — nipkow / hgweb
- fix url/file encoding; — Fabian Huch <huch@in.tum.de> / hgweb
- typo — nipkow / hgweb
- typo — nipkow / hgweb
- tuned metadata — nipkow / hgweb
- tuned metadata — nipkow / hgweb
- tuned metadata — nipkow / hgweb
- merged — paulson / hgweb
- Migration of lemmas to distribution — paulson <lp15@cam.ac.uk> / hgweb
#30 (Sep 29, 2023, 3:18:42 PM)
- merged — wenzelm / hgweb
- adjust Euler_Polyhedron_Formula to AFP-devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from AFP 2023 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- corrected metadata: doi -> acm identifier — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Lovasz_Local and Hypergraph_Basics — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Lovasz_Local — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Hypergraphs — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata and sitegen for Euler Polyhedron Formula — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Euler's Polyhedron Formula — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adapted to Isabelle/72631efa3821; — wenzelm / hgweb
- avoid deadly "handle _ => ..."; — wenzelm / hgweb
- tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
- tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
- tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
- clarified signature, following Isabelle/fde0b195cb7d; — wenzelm / hgweb
- reduced prominence of lemma names — haftmann / hgweb
- merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sync web abstract — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adapted ROOT file link to afp-2023; — Fabian Huch <huch@in.tum.de> / hgweb
- merge from afp-2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- web: 2023 downlaod links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added tag Isabelle2023 for changeset 01bf5fad3e59 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add 2023 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- website regen — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix toml key generated by afp_releases — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- set Isabelle2023 release date — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update Isabelle2022 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- afp release path has changed on isa-afp.org — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix afp-submit for markdown processing — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Moved a general purpose theorem into the main repository — paulson <lp15@cam.ac.uk> / hgweb
- a little fix involving the reformulated version of inclusion/exclusion — paulson <lp15@cam.ac.uk> / hgweb
- fixed missing parenthesis in or-ok-lemma — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new bibiten and titlecase on all sections — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- avoid clones of Isabelle/ML operations --- de-emphasize somewhat old/outdated operation; — wenzelm / hgweb
- replace underscore latex package with formal markup — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- merge — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- fix latex generation — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- Backed out changeset 8eb0a45852dc — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- avoid non-local return; — Fabian Huch <huch@in.tum.de> / hgweb
- removed migration tools; — Fabian Huch <huch@in.tum.de> / hgweb
- follow naming conventions of Isabelle/2a99fcb283ee; — wenzelm / hgweb
- adapted to Isabelle/fd1fec53665b; — wenzelm / hgweb
- Relational_Disjoint_Set_Forests: update history — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- Relational_Disjoint_Set_Forests: minor text edits — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- merged — paulson / hgweb
- small fixes — paulson <lp15@cam.ac.uk> / hgweb
- fix afp-submit for markdown processing — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- switch version back to devel after fork — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- use default AFP chapter settings — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-devel — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update version to 2023 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update author email (by request) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Tree_Enumeration: Fix errors introduced by renamings in Unidrected_Graph_Theory. — Emin Karayel <me@eminkarayel.de> / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sitegen for Fixed_Length_Vector — traytel / hgweb
- added syntax bundles and disabled syntax by default — traytel / hgweb
- moved abstract to root.tex — traytel / hgweb
- made proofs more robust — traytel / hgweb
- new entry Fixed_Length_Vector — traytel / hgweb
- Fixed the title and author of Ceva in the document — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Ceva — paulson <lp15@cam.ac.uk> / hgweb
- new entry Ceva — paulson <lp15@cam.ac.uk> / hgweb
- for better output notation — Akihisa Yamada <akihisa.yamada@aist.go.jp> / hgweb
- regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix duplicated key in IEEE_Floating_Point.toml — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Merge changes — cledmonds / hgweb
- Renamed incident and order to vincident and gorder due to` compatibility issues. — cledmonds / hgweb
- Note recent additions (roundNearestTiesToAway, single NaN value, SMT-LIB translation) in metadata. — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- Merged. — Dominique Unruh <unruh@ut.ee> / hgweb
- Registers: Fixed some broken proofs. — Dominique Unruh <unruh@ut.ee> / hgweb
- redefine substitution of terms as special case of general evaluation of terms — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- 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`. — Dominique Unruh <unruh@ut.ee> / hgweb - update author info — Štěpán Starosta <stepan.starosta@fit.cvut.cz> / hgweb
- Update of Combinatorics_Words, Combinatorics_Words_Graph_Lemma, Combinatorics_Words_Lyndon, Two_Generated_Word_Monoids_Intersection, Binary_Code_Imprimitive to to version v1.10. — Štěpán Starosta <stepan.starosta@fit.cvut.cz> / hgweb
- metadata formatting — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- address metadata warnings — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- remove unused metadata (leaves website unchanged) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Catoids — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- remove obsolete (AFP) group from new entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Word_Lib: import new material from l4v — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update to isabelle@fd8e1bbc0686 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry Polygonal_Number_Theorem — nipkow / hgweb
- Quantales_Converse metadata — paulson <lp15@cam.ac.uk> / hgweb
- new entry Quantales_Converse — paulson <lp15@cam.ac.uk> / hgweb
- Fixed the punctuation in the title and abstract — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser — paulson <lp15@cam.ac.uk> / hgweb
- New entry /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Earley_Parser — paulson <lp15@cam.ac.uk> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned links in theory view; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned instructions; — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- clarify statistics-ignore flag and build example submission properly; — Fabian Huch <huch@in.tum.de> / hgweb
- regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- rectify copy/paste error — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merged — paulson / hgweb
- Redid an ugly proof — paulson <lp15@cam.ac.uk> / hgweb
- construction for anchord GTT intersection
by Alexander Lochman — Gerwin Klein <kleing@unsw.edu.au> / hgweb - merged — paulson / hgweb
- Updated the root file to start from an AFP image — paulson <lp15@cam.ac.uk> / hgweb
- tuned — nipkow / hgweb
- merged — nipkow / hgweb
- new editors Lammich and Traytel — nipkow / hgweb
- Eliminated needless import and rationalised the ROOT file — paulson <lp15@cam.ac.uk> / hgweb
- Deleted needless imports — paulson <lp15@cam.ac.uk> / hgweb
- Generalised and tidied an intermediate result — paulson <lp15@cam.ac.uk> / hgweb
- Higher_Order_Terms: add fresh_list function — Lars Hupel <lars@hupel.info> / hgweb
- delete unneeded file — Lars Hupel <lars@hupel.info> / hgweb
- antiquoting special symbols in text — davfuenmayor@gmail.com / hgweb
- merge with default — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- Relational_Disjoint_Set_Forests: extended theory, refactored related entries — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- Refactored and updated entry. Synchronize with companion paper. — davfuenmayor@gmail.com / hgweb
- simplified proof without auxiliary function — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- provide more unification algorithms, e.g., to compute mgu's modulo variable renamings — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Adapted to devel — nipkow / hgweb
- Relational_Disjoint_Set_Forests: simplified invariant — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- Bell_Numbers_Spivey: Add code equations for the computation of Bell numbers. — Emin Karayel <me@eminkarayel.de> / hgweb
- 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. — Emin Karayel <me@eminkarayel.de> / hgweb - proved a few properties of WPO with less assumption, so that Co-WPO properties can be derived — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Fixed LaTeX. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Merge. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Fixed missing entries in ROOTS file (previous erronous commit). — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Normalised email. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Improved setup of the symbolic evaluator. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Fix proofs broken by previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
- 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. — Emin Karayel <me@eminkarayel.de> / hgweb - merged — paulson / hgweb
- Adjustments for recent cosmetic changes to the Distribution — paulson <lp15@cam.ac.uk> / hgweb
- Proper epsilon-syntax — paulson <lp15@cam.ac.uk> / hgweb
- Merge. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Minor improvement of handling of string literals in symbolic evaluator. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Removing redundant definitions:
- External
- Fallback — dmarmsoler / hgweb - tuned — nipkow / hgweb
- Merge — dmarmsoler / hgweb
- Updating history for Isabelle/Solidity — dmarmsoler / hgweb
- 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. — dmarmsoler / hgweb - Relational_Disjoint_Set_Forests: added a new theory, refactored related entries — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- remove some redundant constraint-types in simplex algorithm — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- relation between has-maximum and bdd_above — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned names — nipkow / hgweb
- merged — nipkow / hgweb
- more comments — nipkow / hgweb
- merged — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- back out Paraconsistency — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- merged — nipkow / hgweb
- tuned and simplified proofs — nipkow / hgweb
- Some additions to IICF by Valentin Springsklee — Peter Lammich / hgweb
- merge — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- small changes in FOL_Seq_Calc1 metadata — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- More Paraconsistency — Anders Schlichtkrull <andsch@cs.aau.dk> / hgweb
- merged — wenzelm / hgweb
- tuned — nipkow / hgweb
- tuned — nipkow / hgweb
- prefer existing Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); — wenzelm / hgweb
- proper .ML file names; — wenzelm / hgweb
- proper .ML file name; — wenzelm / hgweb
- eliminated suspicious Unicode character, which often produce unexpected document output; — wenzelm / hgweb
- eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- avoid hardwired document output; — wenzelm / hgweb
- eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- fixed build following a13761ef6796 — desharna / hgweb
- merged — desharna / hgweb
- removed unnecessary theory with potential for name conflict — desharna / hgweb
- provided var2-versions of all doubly-nested loops — nipkow / hgweb
- Added version of algorithm 4 with precise variant var2 and tuned — nipkow / hgweb
- Floyd Warshall: improve code refinements — Simon Wimmer <wimmers@in.tum.de> / hgweb
- IMP2: fix typos — Simon Wimmer <wimmers@in.tum.de> / hgweb
- New check 'coverage_rcv' added. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- Fixing typos. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb
- 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 — Achim D. Brucker <adbrucker@0x5f.org> / hgweb - typos — nipkow / hgweb
- remove AFP group already defined by chapter; — Fabian Huch <huch@in.tum.de> / hgweb
- Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
#29 (Jul 13, 2023, 8:33:11 PM)
- fix merge problems; — Fabian Huch <huch@in.tum.de> / hgweb
#28 (Jul 13, 2023, 11:21:13 AM)
- merge from afp-2022 — Fabian Huch <huch@in.tum.de> / hgweb
- re-generate site; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned for smaller diffs; — Fabian Huch <huch@in.tum.de> / hgweb
- New topic for Gray_Codes — nipkow / hgweb
- More Gray_Codes — nipkow / hgweb
- More Gray_Codes — nipkow / hgweb
- New entry Gray_Codes — nipkow / hgweb
- metadata and sitegen for Executable_Randomized_Algorithms — paulson <lp15@cam.ac.uk> / hgweb
- New entry Executable_Randomized_Algorithms — paulson <lp15@cam.ac.uk> / hgweb
- new entry DCR-ExecutionEquivalence — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Zeckendorf: metadata and sitegen — paulson <lp15@cam.ac.uk> / hgweb
- new entry Zeckendorf — paulson <lp15@cam.ac.uk> / hgweb
- Crypto_Standards: Fixed a spelling error — paulson <lp15@cam.ac.uk> / hgweb
- Crypto_Standards metadata & website — paulson <lp15@cam.ac.uk> / hgweb
- New entry Crypto_Standards — paulson <lp15@cam.ac.uk> / hgweb
- move TOML module to Isabelle (see Isabelle/be8aaaa4ac25); — Fabian Huch <huch@in.tum.de> / hgweb
- added missing timeout; — Fabian Huch <huch@in.tum.de> / hgweb
- reformat; — Fabian Huch <huch@in.tum.de> / hgweb
- remove duplicate fields; — Fabian Huch <huch@in.tum.de> / hgweb
- check TOML parse structure properly; — Fabian Huch <huch@in.tum.de> / hgweb
- proper typed TOML layer; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned imports; — Fabian Huch <huch@in.tum.de> / hgweb
- Updated links — nipkow / hgweb
- Added citations — nipkow / hgweb
- Added citations — nipkow / hgweb
- Added citations — nipkow / hgweb
- Added refs — nipkow / hgweb
- Added DOIs — nipkow / hgweb
- Added DOIs — nipkow / hgweb
- Added DOIs — nipkow / hgweb
- Added DOI — nipkow / hgweb
- Added DOI — nipkow / hgweb
- added DOI — nipkow / hgweb
- Median_Method: Add a tight version of the median bound, suggested by Yong Kiam Tan. — Emin Karayel <me@eminkarayel.de> / hgweb
- parse proper toml syntax; — Fabian Huch <huch@in.tum.de> / hgweb
- Syntax for symmetric set difference, plus tidying — paulson <lp15@cam.ac.uk> / hgweb
- Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
- Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
- Add — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
- Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
- Update — Yosuke-Ito-345 <glacier345@gmail.com> / hgweb
- merged — paulson / hgweb
- Three_Squares: time limit increase; and now sym_diff is declared in main HOL — paulson <lp15@cam.ac.uk> / hgweb
- moved Subterm_and_Context into First_Order_Terms, merged context of Term_Aux into Term — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- replace scala.sys.process with proper Bash.Process; — Fabian Huch <huch@in.tum.de> / hgweb
- renamed "flatten" to "unindex" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Resolved some operator clashes — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- simplified some proofs — paulson <lp15@cam.ac.uk> / hgweb
- Modifications for moving from f ` S <= T to f:S->T — paulson <lp15@cam.ac.uk> / hgweb
- Updated for new HOL-CSP — Burkhart Wolff <wolff@lri.fr> / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- updated ROOT. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Registers: Fixed nonterminating subproof — Dominique Unruh <unruh@ut.ee> / hgweb
- Collected changes to Complex_Bounded_Operators AFP entry:
Complex_Vector_Spaces.thy
=========================
New lemmas: clinear_scaleR[simp], abs_summable_on_scaleC_left[intro],
abs_summable_on_scaleC_right[intro], ccspan_superset',
ccspan_closure[simp], ccspan_finite, ccspan_UNIV[simp],
infsum_in_closed_csubspaceI,
closed_csubspace_space_as_set[simp], SUP_ccspan
Renamed lemma: bounded_clinear_eq_on -> bounded_clinear_eq_on_closure
Changed typeclass: basis_enum (has additional constant "canonical_basis_length")
Renamed definition: Abs_clinear_space -> Abs_ccsubspace
Complex_Inner_Product.thy
=========================
New lemmas: mem_ortho_ccspanI, basis_projections_reconstruct_has_sum,
basis_projections_reconstruct,
basis_projections_reconstruct_summable,
parseval_identity_has_sum, parseval_identity_summable,
parseval_identity, canonical_basis_is_onb[simp]
Complex_Bounded_Linear_Functions.thy
====================================
New definition: invertible_cblinfun (operator has with left inverse)
New lemmas: not_not_singleton_cblinfun_zero,
cblinfun_norm_approx_witness', summable_on_cblinfun_apply,
summable_on_cblinfun_apply_left,
abs_summable_on_cblinfun_apply_left,
infsum_cblinfun_apply_left, has_sum_cblinfun_apply_left,
bounded_clinear_cblinfun_compose_left,
bounded_clinear_cblinfun_compose_right,
clinear_cblinfun_compose_left,
clinear_cblinfun_compose_right,
additive_cblinfun_compose_left[simp],
additive_cblinfun_compose_right[simp],
isCont_cblinfun_compose_left,
isCont_cblinfun_compose_right, cspan_compose_closed,
cspan_adj_closed, unitaryI, norm_isometry_compose',
unitary_nonzero[simp], isometry_inj, unitary_adj_inv,
isometry_cinner_both_sides, isometry_image_is_ortho_set,
cblinfun_apply_in_image', cblinfun_image_ccspan_leqI,
cblinfun_same_on_image, lift_cblinfun_comp,
cblinfun_image_def2, unitary_image_onb,
sandwich_arg_compose, sandwich_compose,
inj_sandwich_isometry, sandwich_isometry_id,
is_Proj_id[simp], norm_is_Proj_nonzero,
Proj_compose_cancelI, space_as_setI_via_Proj,
unitary_image_ortho_compl, Proj_on_image[simp],
kernel_apply_self, leq_kernel_iff, cblinfun_image_kernel,
cblinfun_image_kernel_unitary, kernel_cblinfun_compose,
eigenspace_0[simp], kernel_isometry,
cblinfun_image_eigenspace_isometry,
cblinfun_image_eigenspace_unitary, kernel_member_iff,
kernel_square[simp], cblinfun_inv_left,
inv_cblinfun_invertible, cblinfun_inv_right,
iso_cblinfun_unitary, invertible_cblinfun_isometry,
summable_cblinfun_apply_invertible,
infsum_cblinfun_apply_invertible, less_eq_scaled_id_norm,
butterflies_sum_id_finite, butterfly_sum_left,
butterfly_sum_right, cblinfun_extension_exists_restrict
Changed lemmas: cblinfun_image_INF_eq_general, cblinfun_image_INF_eq
(more general), positive_hermitianI (flipped sides of
equality), rank1_compose_right, rank1_uminus,
rank1_uminus_iff (more general type class)
Removed lemma: dense_span_separating (use
bounded_clinear_eq_on_closure instead)
Removed bundles: blinfun_notation, no_blinfun_notation
Complex_L2.thy
==============
New lemmas: clinear_Rep_ell2[simp], Abs_ell2_inverse_finite[simp],
norm_ell2_bound_trunc, bounded_clinear_Rep_ell2,
trunc_ell2_singleton, trunc_ell2_insert,
trunc_ell2_finite_sum, is_orthogonal_trunc_ell2,
ell2_decompose_has_sum, ell2_decompose_infsum,
ell2_decompose_summable, Rep_ell2_cblinfun_apply_sum,
explicit_cblinfun_exists,
explicit_cblinfun_exists_bounded,
explicit_cblinfun_exists_finite_dim[simp],
explicit_cblinfun_ket,
Rep_ell2_explicit_cblinfun_ket[simp]
Changed lemmas: cinner_ket (uses "of_bool" instead of "if")
Changed definition: ket (uses "of_bool" instead of "if")
New definition: explicit_cblinfun (define an operator by giving the
entries of an infinite matrix)
Cblinfun_Code:
==============
New definition: butterfly_code
New lemma: butterfly_code
Renamed definition: cblinfun_apply_code -> cblinfun_apply_ell2
Renamed lemmas:
- vec_of_ell2_timesScalarVec -> vec_of_ell2_scaleC
- cinner_ell2_code' -> cinner_ell2_code
- times_ell2_code' -> times_ell2_code
- divide_ell2_code' -> divide_ell2_code
- inverse_ell2_code' -> inverse_ell2_code
- one_ell2_code' -> one_ell2_code
- cblinfun_apply_code -> cblinfun_apply_ell2
- cblinfun_apply_code -> cblinfun_apply_ell2
Cblinfun_Matrix.thy
===================
New lemmas: vec_of_basis_enum_carrier_vec, cblinfun_of_mat_invalid
extra/Extra_General.thy
=======================
New lemmas: not_not_singleton_zero, has_sumI_metric,
limitin_pullback_topology, tendsto_coordinatewise,
limitin_closure_of
extra/Extra_Vector_Spaces.thy
=============================
New lemmas: summable_on_bounded_linear, any_norm_exists,
abs_summable_on_scaleR_left[intro],
abs_summable_on_scaleR_right[intro],
Changed lemma: enum_idx_bound (expressed using CARD, added [simp])
extra/Extra_Jordan_Normal_Form.thy
==================================
New lemmas: map_map_vec_cols, map_vec_conjugate — Dominique Unruh <unruh@ut.ee> / hgweb - Renamings of operators, and a major theorem on distributivity of Mprefix vs Sync. Renamings of some lemmata. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Updated metadata for several entries.
- Updated categorization for derandomization libraries, based on the newly introduced CS/Alg./Randomized category.
- Added related reference for Nils Cremer's Tree Enumeration
- Removed obsolete comments in Expander Grapgs — Emin Karayel <me@eminkarayel.de> / hgweb - metadata and sitegen for Directed_Sets — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Directed_Sets — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from AFP 2022 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata and sitegen for Multirelations_Heterogeneous — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Multirelations_Heterogeneous — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjust Schwartz_Zippel entry
- Use Pi_pmf from HOL-Probability
- Generalize theorem(s) in example — Yong Kiam Tan <yongkiat@cs.cmu.edu> / hgweb - adjusted Simple_Clause_Learning from AFP 2022 to AFP devel — desharna / hgweb
- adjusted Given_Clause_Loops from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted CommCSL from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted DigitsInBase from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted Schwartz_Zippel from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted TsirelsonBound from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted Tree_Enumeration from AFP 2022 to AFP devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted efficient WPO from AFP 2022 to afp devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from afp-2022 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry Efficient_Weighted_Path_Order — nipkow / hgweb
- add edit mode to afp-submit UI; — Fabian Huch <huch@in.tum.de> / hgweb
- solved subtle problem with multiple entries and new authors; — Fabian Huch <huch@in.tum.de> / hgweb
- better error logging; — Fabian Huch <huch@in.tum.de> / hgweb
- added edit handler to submission app; — Fabian Huch <huch@in.tum.de> / hgweb
- added frontend in devel mode; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned (mostly api path handling); — Fabian Huch <huch@in.tum.de> / hgweb
- A real title in place of MLSS_Decision_Proc — paulson <lp15@cam.ac.uk> / hgweb
- MLSS_Decision_Proc sitegen — paulson <lp15@cam.ac.uk> / hgweb
- New entry MLSS_Decision_Proc — paulson <lp15@cam.ac.uk> / hgweb
- metadata and sitegen for TsirelsonBound — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: TsirelsonBound — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry Tree_Enumeration — nipkow / hgweb
- Three_Squares citegen — paulson <lp15@cam.ac.uk> / hgweb
- New entry Three_Squares — paulson <lp15@cam.ac.uk> / hgweb
- fixed some ACM/AMS categories — Manuel Eberl <manuel@pruvisto.org> / hgweb
- more files — nipkow / hgweb
- New entry MHComputation — nipkow / hgweb
- make index.json files line-by-line for smaller diffs; — Fabian Huch <huch@in.tum.de> / hgweb
- cleanup; — Fabian Huch <huch@in.tum.de> / hgweb
- added new entry DigitsInBase; — Fabian Huch <huch@in.tum.de> / hgweb
- fixed broken LaTeX quotation marks in abstracts — Manuel Eberl <eberlm@in.tum.de> / hgweb
- recategorised some entries — Manuel Eberl <eberlm@in.tum.de> / hgweb
- new topic: Computer science/Algorithms/Randomized — Manuel Eberl <eberlm@in.tum.de> / hgweb
- sitegen for Schwartz_Zippel — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry: Schwartz_Zippel — Manuel Eberl <manuel@pruvisto.org> / hgweb
- New entry: Simple_Clause_Learning — nipkow / hgweb
- New entry HyperHoareLogic — nipkow / hgweb
- New entry Distributed_Distinct_Elements — nipkow / hgweb
- metadata for CommCSL + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: CommCSL — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry No_FTL_observers_Gen_Rel — nipkow / hgweb
- added new files generated by sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Expander Graphs — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Expander Graphs — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- fix of toml-entries and rerun of sitegen: problem: links where in these quotes: ”...” and not in the standard ones "..." — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen (for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Two_Generated_Word_Monoids_Intersection — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Binary_Code_Imprimitive — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- running sort on ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry Probability_Inequality_Completeness — nipkow / hgweb
- Rensets metadata — paulson / hgweb
- New entry Rensets — paulson <lp15@cam.ac.uk> / hgweb
- more Edwards — nipkow / hgweb
- New entry Edwards_Elliptic_Curves_Group — nipkow / hgweb
- metadata and sitegen for CVP_Hardness — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: CVP_Hardness — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- rerun sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- revert proof compression experiment — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata for ABY3_Protocols — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry ABY3_Protocols — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- sitegen for Given_Clause_Loops — paulson <lp15@cam.ac.uk> / hgweb
- New entry Given_Clause_Loops — paulson <lp15@cam.ac.uk> / hgweb
- Adjustments for the simplified version of real_le_lsqrt — paulson <lp15@cam.ac.uk> / hgweb
- adapted to Isabelle/84a7a0029c82 — desharna / hgweb
- merged — desharna / hgweb
- adapted to Isabelle/0252d635bfb2 — desharna / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- Merge with developper version on LISN gut — Burkhart Wolff <wolff@lri.fr> / hgweb
- merged — wenzelm / hgweb
- prefer @{attributes} antiquotation over Attrib.internal;
adapted to Isabelle/bc42c074e58f; — wenzelm / hgweb - tuned proofs; — wenzelm / hgweb
- Deleted a superfluous assumption. This proof is a horror — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- fixed some bibliographic entries — paulson <lp15@cam.ac.uk> / hgweb
- merged — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- tuned — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- merged — wenzelm / hgweb
- merged — wenzelm / hgweb
- adapted to current Isabelle/ec1c0daa3fbd; — wenzelm / hgweb
- adapted to current Isabelle/ec1c0daa3fbd; — wenzelm / hgweb
- adapted to Isabelle/5edd5b12017d; — wenzelm / hgweb
- proper morphism context; — wenzelm / hgweb
- backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531; — wenzelm / hgweb
- proper morphism context; — wenzelm / hgweb
- adapted to Isabelle/5ab5add88922; — wenzelm / hgweb
- SMT-LIB interpretation of floating-point arithmetic — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- merged — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- SMT-LIB interpretation of floating-point arithmetic — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- IEEE model with a single NaN value — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- Minor — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- merging — JeremyDubut <dubutjeremy@gmail.com> / hgweb
- updates for future formalizations — JeremyDubut <dubutjeremy@gmail.com> / hgweb
- adapted to Isabelle/f78cdc6fe971; — wenzelm / hgweb
- adapted to Isabelle/f78cdc6fe971; — wenzelm / hgweb
- A slight beautification — paulson <lp15@cam.ac.uk> / hgweb
- adapted to 3f354d5bbf98; — wenzelm / hgweb
- Rounding modes renamed — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- merged — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- Add the rounding mode roundNearestTiesToAway. — Tjark Weber <tjark.weber@it.uu.se> / hgweb
- Merge realtime deque renamings — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- simplify some measurements — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- rename Deque.Idle to Idles — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- Rename Big and Small cases — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- rename `Transforming` to `Rebal` — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- rename `Common.state` to `common_state` — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- rename Small.state to small_state — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- rename Big.state to big_state — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- backed out changeset 2ecb8f5e085f: obsolete thanks to Isabelle/21cdcd120a78; — wenzelm / hgweb
- more robust: make it work with Isabelle/a12c48fbf10f; — wenzelm / hgweb
- adapted to Isabelle/c4677a6aae2c; — wenzelm / hgweb
- adapted to Isabelle/c4677a6aae2c; — wenzelm / hgweb
#27 (May 5, 2023, 10:30:08 AM)
- modificaiton due to latex — nanjiang <nanjiang@whu.edu.cn> / hgweb
- some small modifications — nanjiang <nanjiang@whu.edu.cn> / hgweb
#26 (May 4, 2023, 2:11:51 PM)
- merged — Fabian Huch <huch@in.tum.de> / hgweb
- Some hyphens that should be en dashes — paulson <lp15@cam.ac.uk> / hgweb
- slightly refine WPO-definition
- previous formalization of WPO deviated a bit to paper version (requiring less computation)
- both versions are equivalent whenever order in parameter is strongly normalizing
- however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders
- consequence: change formalization so that it is more closely related to paper version,
so that also results on coWPO can be proven — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb - merged — wenzelm / hgweb
- no "open" of ML structures: it makes sources unmaintainable; — wenzelm / hgweb
- adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
- adapted to Isabelle/f4cd6e3b5075; — wenzelm / hgweb
- adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
- This file should have been removed in the previous commit. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Sync with my development repo. Main changes related to CartesianMonoidalCategory. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- update timing; — wenzelm / hgweb
- eliminated pointless parallelism: approx. 1.3s as plain sequential ML; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp; — wenzelm / hgweb
- adapted to Isabelle/c274f52b11ff; — wenzelm / hgweb
- Backed out changeset a537fb4c92af — wenzelm / hgweb
- slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d; — wenzelm / hgweb
- merged — nipkow / hgweb
- moved lemma to FDS exercises — nipkow / hgweb
- Fix proofs broken by previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
- Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad
The rule is necessary for the termination proof of some recursive functions
over the time monad. — Emin Karayel <me@eminkarayel.de> / hgweb - tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- eliminated aliases: prefer existing Thm.elim_implies; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more standard use of structure Unsynchronized; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- not unused! — nipkow / hgweb
- Added running time analysis — nipkow / hgweb
- some remarks on division — haftmann / hgweb
- clarified scope of document — haftmann / hgweb
- no subsection without section — haftmann / hgweb
- merged — paulson / hgweb
- Deleted library material — paulson <lp15@cam.ac.uk> / hgweb
- adapted to Isabelle/b43ee37926a9; — wenzelm / hgweb
- merged — wenzelm / hgweb
- adapted to Isabelle/13cee8c2ed8d; — wenzelm / hgweb
- Add related entry for Combinatorial_Enumeration_Algorithms.
Note: I followed APA style guide for the reference. https://apastyle.apa.org/style-grammar-guidelines/references/examples/published-dissertation-references
Note: Ran sitegen. — Emin Karayel <me@eminkarayel.de> / hgweb - small simplifications — blanchet / hgweb
- shortened some parts of Huffman proof using Sledgehammer — blanchet / hgweb
- added another simplification rule when alternatives are equal — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added more simplification rules involving Zero — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- adapted to Isabelle/4a174bea55e2; — wenzelm / hgweb
- uodated map update syntax — nipkow / hgweb
- Adjusted to changes in distribution. — haftmann / hgweb
- more realistic timeout; — wenzelm / hgweb
- avoid hardwired documents;
tuned whitespace; — wenzelm / hgweb - merged — paulson / hgweb
- simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
- added character sets to the extension directory of regular expressions — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- more syntax adjustments — nipkow / hgweb
- more syntax update for map update syntax — nipkow / hgweb
- more map update syntax updates — nipkow / hgweb
- merged — nipkow / hgweb
- updated to new map update syntax priorities — nipkow / hgweb
- Some simplifications of proofs — paulson <lp15@cam.ac.uk> / hgweb
- Minor refinements — paulson <lp15@cam.ac.uk> / hgweb
- tiny simplifications — paulson <lp15@cam.ac.uk> / hgweb
- tidied another file — paulson <lp15@cam.ac.uk> / hgweb
- tidied a bit more — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- More tidying — paulson <lp15@cam.ac.uk> / hgweb
- completed the addtion of Rec in the Extension directory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added another regular expression for Record — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- More tidying of the Ordinal entry — paulson <lp15@cam.ac.uk> / hgweb
- A massive tidying — paulson <lp15@cam.ac.uk> / hgweb
- Tiny bit more tidying — paulson <lp15@cam.ac.uk> / hgweb
- more robust: allow optional arguments in isabelle.Progress.echo; — wenzelm / hgweb
- More tidying — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Suppression of duplicate syntax for abs_summable_on, etc. — paulson <lp15@cam.ac.uk> / hgweb
- No more sorted_take, sorted_drop — paulson <lp15@cam.ac.uk> / hgweb
- Update entries MDP-Rewards and MDP-Algorithms — Maximilian Schaeffeler <maximilian.schaeffeler@tum.de> / hgweb
- Migration of material from Jordan_Hoelder to HOL-Algebra — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Tidied up some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- Adjustments for the new infix status of has_sum — paulson <lp15@cam.ac.uk> / hgweb
- A tiny spelling correction — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- A little more migration — paulson <lp15@cam.ac.uk> / hgweb
- Backed out changeset fa59c080cb3b — nipkow / hgweb
- Backed out changeset 811f0b8d4f58 — nipkow / hgweb
- tuned metis call to avoid obscure feature — blanchet / hgweb
- merged — paulson / hgweb
- Migration of material to the repository and necessary modifications — paulson <lp15@cam.ac.uk> / hgweb
- more map_of adaptions — nipkow / hgweb
- adapted to new List.map_of — nipkow / hgweb
- update Real_Time_Deque — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- Removal of a stray sledgehammer command — paulson <lp15@cam.ac.uk> / hgweb
- explicit range types in abstractions — stuebinm <stuebinm@disroot.org> / hgweb
- somehow more clear terminology — haftmann / hgweb
- merged — paulson / hgweb
- Some tidying and moving some material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
- Deleted use of Euclidean_Division — Katharina Kreuzer / hgweb
- Repaired session name — Katharina Kreuzer / hgweb
- "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium" — Katharina Kreuzer / hgweb
- Update names to match thesis. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions; — wenzelm / hgweb
- proper symbolic handle on component resources (see Isabelle/3eb3de867786); — wenzelm / hgweb
- more realistic timeout, based on CPU time; — wenzelm / hgweb
- adapted to Isabelle/9a60c1759543; — wenzelm / hgweb
- more realistic timeout, based on CPU time; — wenzelm / hgweb
- fixed looping proofs — paulson <lp15@cam.ac.uk> / hgweb
- dropped reference to dead clone — haftmann / hgweb
- removed dead clone — haftmann / hgweb
- modernized — haftmann / hgweb
- Modernized. — haftmann / hgweb
- More instances. — haftmann / hgweb
- Tuned whitespace. — haftmann / hgweb
- Updated references. — haftmann / hgweb
- More correct references. — haftmann / hgweb
- Removed a bit of unnecessary material — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Shortened several messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- Fix name clash in Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
- Fixed a name clash — paulson <lp15@cam.ac.uk> / hgweb
- Moving more material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
- Moving some material to the main repository — paulson <lp15@cam.ac.uk> / hgweb
- adapted to db93f67a; — Fabian Huch <huch@in.tum.de> / hgweb
- merged — Fabian Huch <huch@in.tum.de> / hgweb
- generalized theory name: euclidean division denotes one particular division definition on integers — haftmann / hgweb
- more efficient specification — haftmann / hgweb
- merge from afp-2022 — Fabian Huch <huch@in.tum.de> / hgweb
- metadata for Suppes' theorem + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Suppes' Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry HoareForDivergence — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
- metadat for StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
- cleanup accidental unused document files; — Fabian Huch <huch@in.tum.de> / hgweb
- check ROOTs: add warning-only checks; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- add ROOT checks for document presence and unused files; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit visual improvements; — Fabian Huch <huch@in.tum.de> / hgweb
- update bibtex example; — Fabian Huch <huch@in.tum.de> / hgweb
- new doi — nipkow / hgweb
- sitegen for AOT — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- New entry AOT — paulson <lp15@cam.ac.uk> / hgweb
- New entry: Propositional_Logic_Class — nipkow / hgweb
- sitegen for Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
- New entry Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
- Sorry — extra files for Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
- Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
- New entry Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
- New entry: Synthetic_Completeness — nipkow / hgweb
- New entry: Quantifier_Elimination_Hybrid — nipkow / hgweb
- New entry Birkhoff_Finite_Distributive_Lattices — nipkow / hgweb
- sitegen for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Turan — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added metadata for Turans graph theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Turans Graph Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry Multitape_To_Singletape_TM — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- removed static pages from rss feed; — Fabian Huch <huch@in.tum.de> / hgweb
- Minor rerating of the abstract of Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
- New entry Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for the aforementioned changes — paulson <lp15@cam.ac.uk> / hgweb
- adjustments to the abstract, requested by the author — paulson <lp15@cam.ac.uk> / hgweb
- CHERI-C_Memory_Model patch & metadata — paulson <lp15@cam.ac.uk> / hgweb
- New submission CHERI-C_Memory_Model — paulson <lp15@cam.ac.uk> / hgweb
- updated docs; — Fabian Huch <huch@in.tum.de> / hgweb
- improve page layout slightly; — Fabian Huch <huch@in.tum.de> / hgweb
- fixed broken abstract for PAPP_Impossibility — Manuel Eberl <manuel@pruvisto.org> / hgweb
- remove dead code — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- remove old .sitegen-ignore and mention AFP chapter in submission guidelines; — Fabian Huch <huch@in.tum.de> / hgweb
- afp_check_roots: proper error message printing; — Fabian Huch <huch@in.tum.de> / hgweb
- metadata and sitegen for Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned check names; — Fabian Huch <huch@in.tum.de> / hgweb
- make check roots tool less dependent on AFP structure; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- web for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
- sitegen for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
- New entry Combinatorial_Enumeration_Algorithms — nipkow / hgweb
- fix duplicate affiliations from author and notify; — Fabian Huch <huch@in.tum.de> / hgweb
- add metadata check tool to sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- update check tools: add formatting checks, new cmd options; — Fabian Huch <huch@in.tum.de> / hgweb
- check for entries instead of session due to session nesting allowed in entries; — Fabian Huch <huch@in.tum.de> / hgweb
- added unused thy check; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified check roots tool; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: encode new notify addresses properly; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: correct build status on empty file; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: remove padding on select; — Fabian Huch <huch@in.tum.de> / hgweb
- re-format metadata; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: update on correct status change; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: clarified date format, tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
- switch fonts to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
- switch to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp-submit error handling; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp-submit creation and message; — Fabian Huch <huch@in.tum.de> / hgweb
- list submission system website; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: clarified api urls; — Fabian Huch <huch@in.tum.de> / hgweb
- Removal of more unused material — paulson <lp15@cam.ac.uk> / hgweb
- Small simplifications. Removed a needless assumption. — paulson <lp15@cam.ac.uk> / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc; — wenzelm / hgweb
- Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author) — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Added the missing .bib file — paulson <lp15@cam.ac.uk> / hgweb
- proper bib context for formal citations, although there is no document; — wenzelm / hgweb
- back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
- back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
- back to unchecked \cite: there is entry lacks .bib file; — wenzelm / hgweb
- proper citation; — wenzelm / hgweb
- merged — desharna / hgweb
- added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp] — desharna / hgweb
- merged — wenzelm / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
- consistent casing in \cite — Lars Hupel <lars.hupel@mytum.de> / hgweb
- ETTS: updated bibliography and citations — user9716869 <user9716869@gmail.com> / hgweb
- merged — wenzelm / hgweb
- more correct and complete citations; — wenzelm / hgweb
- unchecked \cite for unidentifiable citation; — wenzelm / hgweb
- proper @{cite} syntax; — wenzelm / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- Updating Risk Free Lending Entry
- Adding lemma for transfers in special case
- Fixing grammar in abstract
- Adding citation — Matthew Doty <matt@w-d.org> / hgweb - added bibliography to ROOT; — Fabian Huch <huch@in.tum.de> / hgweb
- CTR and ETTS: several amendments (fact names, printing, presentation) — user9716869 <user9716869@gmail.com> / hgweb
- Removed a reference to the (redundant) wf_restr — paulson <lp15@cam.ac.uk> / hgweb
- added bibliographies to ROOTs; — Fabian Huch <huch@in.tum.de> / hgweb
- Changes for generalised lemmas — Katharina Kreuzer / hgweb
- Changes for generalised lemmas — Katharina Kreuzer / hgweb
- Generalised Lemmas — Katharina Kreuzer / hgweb
- merged — desharna / hgweb
- adapted to Isabelle/c9e091867206 — desharna / hgweb
- tuned; — wenzelm / hgweb
- tuned signature, following Isabelle/947510ce4e36; — wenzelm / hgweb
- adapted to Isabelle/25900fbea7ad;
fewer clones of Isabelle sources; — wenzelm / hgweb - adapted to Isabelle/b61ad889dffa — desharna / hgweb
- removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL — desharna / hgweb
- merged — desharna / hgweb
- adapted to Isabelle/d33fc5228aae — desharna / hgweb
- fixed proof following Isabelle/66cae055ac7b — desharna / hgweb
- merge — blanchet / hgweb
- adapted to Isabelle/c48fe2be847f — blanchet / hgweb
- enable -no-pie for CakeML — Lars Hupel <lars.hupel@mytum.de> / hgweb
- fixed proofs and removed duplicates following Isabelle/e65a50f6c2de — desharna / hgweb
- tuned proofs to use asymI, asymD, asympI, and asympD — desharna / hgweb
- Fix failing continuous integration — desharna / hgweb
- fixed proof following Isabelle/8fff4e4d81cb — desharna / hgweb
- removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL — desharna / hgweb
- added lemma imgu_range_vars_subset — desharna / hgweb
- Update headers and metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fix ROOT again — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fix ROOT — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fixed proofs following Isabelle/a7d2a7a737b8 — desharna / hgweb
- added lemmas mem_range_varsI and imgu_subst_domain_subset — desharna / hgweb
- weakened the definition of redundant_inference — desharna / hgweb
- removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL — desharna / hgweb
- fixed Containers following introduction of irrefl_on — desharna / hgweb
- added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset — desharna / hgweb
- name change — nipkow / hgweb
- AFP and DBLP — nipkow / hgweb
- merged — desharna / hgweb
- added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset — desharna / hgweb
- added lemma subst_domain_rename_subst_domain_subset — desharna / hgweb
- added lemma image_the_Var_image_subst_renaming_eq — desharna / hgweb
- Added acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
- Added code export to ROOT — mohammadabdulaziz / hgweb
- Removed out of place code — mohammadabdulaziz / hgweb
- tuned lemma subst_domain_restrict_subst_domain — desharna / hgweb
- added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp] — desharna / hgweb
- added attribute [simp] to lemma rename_subst_domain_Var_rhs — desharna / hgweb
- added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp] — desharna / hgweb
- merged — desharna / hgweb
- removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL — desharna / hgweb
- removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL — desharna / hgweb
- added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp] — desharna / hgweb
- added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset — desharna / hgweb
- Streamlined a proof — paulson <lp15@cam.ac.uk> / hgweb
- added lemmas — desharna / hgweb
- moved lemma around — desharna / hgweb
- redefined mgu as a definition — desharna / hgweb
- tuned naming — desharna / hgweb
- fixed proof — desharna / hgweb
- added definition restrict_subst_domain and associated lemmas — desharna / hgweb
- tuned (sub)subsection — desharna / hgweb
- added lemma member_image_the_Var_image_subst — desharna / hgweb
- added lemmas unify_subst_domain_range_vars_disjoint — desharna / hgweb
- added lemma unify_range_vars — desharna / hgweb
- added lemma unify_subst_domain — desharna / hgweb
- added definition rename_subst_domain_range and related lemmas — desharna / hgweb
- merged — desharna / hgweb
- added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset — desharna / hgweb
- Fixed the ROOT file, so that the theory of cardinals is loaded — paulson <lp15@cam.ac.uk> / hgweb
- added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term — desharna / hgweb
- added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same — desharna / hgweb
- added lemma decompose_same_Fun[simp] — desharna / hgweb
- added lemma zip_option_same[simp] — desharna / hgweb
- added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain — desharna / hgweb
- removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
- used rho for renamming — desharna / hgweb
- tuned assumptions — desharna / hgweb
- added lemma subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
- added lemmas inv_renaming_sound and ex_inverse_of_renaming — desharna / hgweb
- added lemma subst_apply_term_ident — desharna / hgweb
- added lemmas subst_range_Var and range_vars_Var and moved stuff around — desharna / hgweb
- added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming — desharna / hgweb
- tuned naming — desharna / hgweb
- added lemma mgu_range_vars — desharna / hgweb
- added lemma subst_compose_apply_eq_apply_lhs_if — desharna / hgweb
- added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu — desharna / hgweb
- RealTimeDeque: replace `reverseN` with `take_rev — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on — desharna / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add missing thy files in Sturm_Tarski + repair — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- afp-submit: style page, improve elements; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: added repository updates; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: added download and faster file handling; — Fabian Huch <huch@in.tum.de> / hgweb
- add submission pages to web ui; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: add submission and build status with adapter to existing system; — Fabian Huch <huch@in.tum.de> / hgweb
- add user-facing exception handling to web app; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified submission handling; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: added submission read-only and list views; — Fabian Huch <huch@in.tum.de> / hgweb
- add afp-submit web app; — Fabian Huch <huch@in.tum.de> / hgweb
- add web app facilities; — Fabian Huch <huch@in.tum.de> / hgweb
- RealTimeDeque: Separate implementation and auxiliary functions — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- Backed out changeset 3a67df508397
The finite simproc is no longer active by default — nipkow / hgweb - adapted to new simproc finite — nipkow / hgweb
- clarified signature, following Isabelle/f362975e8ba1; — wenzelm / hgweb
- more direct Proof_Context.init_global; — wenzelm / hgweb
- proper naming conventions for Isabelle/ML; — wenzelm / hgweb
- Updated citation — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Isabelle2022: new release download links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added tag Isabelle2022 for changeset 548e384c0445 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Removal of some old junk — paulson <lp15@cam.ac.uk> / hgweb
- Deleted unused material — paulson <lp15@cam.ac.uk> / hgweb
- nothing — paulson <lp15@cam.ac.uk> / hgweb
- Instantiation of the order solver for ⊑ and ⊏ (no real effect though) — paulson <lp15@cam.ac.uk> / hgweb
- proof simplifications — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Simplified the proofs a bit — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- replaced fmember.rep_eq by fmember_iff_member_fset — desharna / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- adapted to Isabelle/457f1cba78fb — desharna / hgweb
- merged — desharna / hgweb
- added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;
added simp annotation to generalizes_refl — desharna / hgweb - extracted proof cases from lifting_lemma to distinct lemmas — desharna / hgweb
- tuned proof due to new simp rules — nipkow / hgweb
- corresponding lemma was removed from distribution — nipkow / hgweb
#24 (May 4, 2023, 1:57:09 PM)
- some small modifications — nanjiang <nanjiang@whu.edu.cn> / hgweb
#23 (May 3, 2023, 11:21:29 AM)
- Some hyphens that should be en dashes — paulson <lp15@cam.ac.uk> / hgweb
- slightly refine WPO-definition
- previous formalization of WPO deviated a bit to paper version (requiring less computation)
- both versions are equivalent whenever order in parameter is strongly normalizing
- however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders
- consequence: change formalization so that it is more closely related to paper version,
so that also results on coWPO can be proven — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb - merged — wenzelm / hgweb
- no "open" of ML structures: it makes sources unmaintainable; — wenzelm / hgweb
- adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
- adapted to Isabelle/f4cd6e3b5075; — wenzelm / hgweb
- adapted to Isabelle/5db014c36f42; — wenzelm / hgweb
- This file should have been removed in the previous commit. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Sync with my development repo. Main changes related to CartesianMonoidalCategory. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- update timing; — wenzelm / hgweb
- eliminated pointless parallelism: approx. 1.3s as plain sequential ML; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- alternative version by Manuel Eberl, following the approach of Isabelle2022/src/HOL/Tools/sat.ML with one big hyp; — wenzelm / hgweb
- adapted to Isabelle/c274f52b11ff; — wenzelm / hgweb
- Backed out changeset a537fb4c92af — wenzelm / hgweb
- slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d; — wenzelm / hgweb
- merged — nipkow / hgweb
- moved lemma to FDS exercises — nipkow / hgweb
- Fix proofs broken by previous commit. — Emin Karayel <me@eminkarayel.de> / hgweb
- Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad
The rule is necessary for the termination proof of some recursive functions
over the time monad. — Emin Karayel <me@eminkarayel.de> / hgweb - tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- eliminated aliases: prefer existing Thm.elim_implies; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more standard use of structure Unsynchronized; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- not unused! — nipkow / hgweb
- Added running time analysis — nipkow / hgweb
- some remarks on division — haftmann / hgweb
- clarified scope of document — haftmann / hgweb
- no subsection without section — haftmann / hgweb
- merged — paulson / hgweb
- Deleted library material — paulson <lp15@cam.ac.uk> / hgweb
- adapted to Isabelle/b43ee37926a9; — wenzelm / hgweb
- merged — wenzelm / hgweb
- adapted to Isabelle/13cee8c2ed8d; — wenzelm / hgweb
- Add related entry for Combinatorial_Enumeration_Algorithms.
Note: I followed APA style guide for the reference. https://apastyle.apa.org/style-grammar-guidelines/references/examples/published-dissertation-references
Note: Ran sitegen. — Emin Karayel <me@eminkarayel.de> / hgweb - small simplifications — blanchet / hgweb
- shortened some parts of Huffman proof using Sledgehammer — blanchet / hgweb
- added another simplification rule when alternatives are equal — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added more simplification rules involving Zero — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- adapted to Isabelle/4a174bea55e2; — wenzelm / hgweb
- uodated map update syntax — nipkow / hgweb
- Adjusted to changes in distribution. — haftmann / hgweb
- more realistic timeout; — wenzelm / hgweb
- avoid hardwired documents;
tuned whitespace; — wenzelm / hgweb - merged — paulson / hgweb
- simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
- added character sets to the extension directory of regular expressions — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- more syntax adjustments — nipkow / hgweb
- more syntax update for map update syntax — nipkow / hgweb
- more map update syntax updates — nipkow / hgweb
- merged — nipkow / hgweb
- updated to new map update syntax priorities — nipkow / hgweb
- Some simplifications of proofs — paulson <lp15@cam.ac.uk> / hgweb
- Minor refinements — paulson <lp15@cam.ac.uk> / hgweb
- tiny simplifications — paulson <lp15@cam.ac.uk> / hgweb
- tidied another file — paulson <lp15@cam.ac.uk> / hgweb
- tidied a bit more — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- More tidying — paulson <lp15@cam.ac.uk> / hgweb
- completed the addtion of Rec in the Extension directory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added another regular expression for Record — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- More tidying of the Ordinal entry — paulson <lp15@cam.ac.uk> / hgweb
- A massive tidying — paulson <lp15@cam.ac.uk> / hgweb
- Tiny bit more tidying — paulson <lp15@cam.ac.uk> / hgweb
- more robust: allow optional arguments in isabelle.Progress.echo; — wenzelm / hgweb
- More tidying — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Suppression of duplicate syntax for abs_summable_on, etc. — paulson <lp15@cam.ac.uk> / hgweb
- No more sorted_take, sorted_drop — paulson <lp15@cam.ac.uk> / hgweb
- Update entries MDP-Rewards and MDP-Algorithms — Maximilian Schaeffeler <maximilian.schaeffeler@tum.de> / hgweb
- Migration of material from Jordan_Hoelder to HOL-Algebra — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Tidied up some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- Adjustments for the new infix status of has_sum — paulson <lp15@cam.ac.uk> / hgweb
- A tiny spelling correction — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- A little more migration — paulson <lp15@cam.ac.uk> / hgweb
- Backed out changeset fa59c080cb3b — nipkow / hgweb
- Backed out changeset 811f0b8d4f58 — nipkow / hgweb
- tuned metis call to avoid obscure feature — blanchet / hgweb
- merged — paulson / hgweb
- Migration of material to the repository and necessary modifications — paulson <lp15@cam.ac.uk> / hgweb
- more map_of adaptions — nipkow / hgweb
- adapted to new List.map_of — nipkow / hgweb
- update Real_Time_Deque — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- Removal of a stray sledgehammer command — paulson <lp15@cam.ac.uk> / hgweb
- explicit range types in abstractions — stuebinm <stuebinm@disroot.org> / hgweb
- somehow more clear terminology — haftmann / hgweb
- merged — paulson / hgweb
- Some tidying and moving some material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
- Deleted use of Euclidean_Division — Katharina Kreuzer / hgweb
- Repaired session name — Katharina Kreuzer / hgweb
- "Repaired boundary behaviour of mod+- for even modulus, Added locale module_spec for possible instantiation of Dilithium" — Katharina Kreuzer / hgweb
- Update names to match thesis. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- proper components base, following "isabelle components -I": downloaded components should be shared for all Isabelle versions; — wenzelm / hgweb
- proper symbolic handle on component resources (see Isabelle/3eb3de867786); — wenzelm / hgweb
- more realistic timeout, based on CPU time; — wenzelm / hgweb
- adapted to Isabelle/9a60c1759543; — wenzelm / hgweb
- more realistic timeout, based on CPU time; — wenzelm / hgweb
- fixed looping proofs — paulson <lp15@cam.ac.uk> / hgweb
- dropped reference to dead clone — haftmann / hgweb
- removed dead clone — haftmann / hgweb
- modernized — haftmann / hgweb
- Modernized. — haftmann / hgweb
- More instances. — haftmann / hgweb
- Tuned whitespace. — haftmann / hgweb
- Updated references. — haftmann / hgweb
- More correct references. — haftmann / hgweb
- Removed a bit of unnecessary material — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Shortened several messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- Fix name clash in Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
- Fixed a name clash — paulson <lp15@cam.ac.uk> / hgweb
- Moving more material to the distribution — paulson <lp15@cam.ac.uk> / hgweb
- Moving some material to the main repository — paulson <lp15@cam.ac.uk> / hgweb
- adapted to db93f67a; — Fabian Huch <huch@in.tum.de> / hgweb
- merged — Fabian Huch <huch@in.tum.de> / hgweb
- generalized theory name: euclidean division denotes one particular division definition on integers — haftmann / hgweb
- more efficient specification — haftmann / hgweb
- merge from afp-2022 — Fabian Huch <huch@in.tum.de> / hgweb
- metadata for Suppes' theorem + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Suppes' Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry HoareForDivergence — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
- metadat for StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry StrictOmegaCategories — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- tuned css; — Fabian Huch <huch@in.tum.de> / hgweb
- cleanup accidental unused document files; — Fabian Huch <huch@in.tum.de> / hgweb
- check ROOTs: add warning-only checks; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- add ROOT checks for document presence and unused files; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit visual improvements; — Fabian Huch <huch@in.tum.de> / hgweb
- update bibtex example; — Fabian Huch <huch@in.tum.de> / hgweb
- new doi — nipkow / hgweb
- sitegen for AOT — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- New entry AOT — paulson <lp15@cam.ac.uk> / hgweb
- New entry: Propositional_Logic_Class — nipkow / hgweb
- sitegen for Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
- New entry Cook_Levin — paulson <lp15@cam.ac.uk> / hgweb
- Sorry — extra files for Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
- Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
- New entry Boolos_Curious_Inference_Automated — paulson <lp15@cam.ac.uk> / hgweb
- New entry: Synthetic_Completeness — nipkow / hgweb
- New entry: Quantifier_Elimination_Hybrid — nipkow / hgweb
- New entry Birkhoff_Finite_Distributive_Lattices — nipkow / hgweb
- sitegen for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Kneser_Cauchy_Davenport — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Turan — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added metadata for Turans graph theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Turans Graph Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry Multitape_To_Singletape_TM — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- removed static pages from rss feed; — Fabian Huch <huch@in.tum.de> / hgweb
- Minor rerating of the abstract of Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
- New entry Sauer_Shelah_Lemma — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for the aforementioned changes — paulson <lp15@cam.ac.uk> / hgweb
- adjustments to the abstract, requested by the author — paulson <lp15@cam.ac.uk> / hgweb
- CHERI-C_Memory_Model patch & metadata — paulson <lp15@cam.ac.uk> / hgweb
- New submission CHERI-C_Memory_Model — paulson <lp15@cam.ac.uk> / hgweb
- updated docs; — Fabian Huch <huch@in.tum.de> / hgweb
- improve page layout slightly; — Fabian Huch <huch@in.tum.de> / hgweb
- fixed broken abstract for PAPP_Impossibility — Manuel Eberl <manuel@pruvisto.org> / hgweb
- remove dead code — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry PAPP_Impossibility — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- remove old .sitegen-ignore and mention AFP chapter in submission guidelines; — Fabian Huch <huch@in.tum.de> / hgweb
- afp_check_roots: proper error message printing; — Fabian Huch <huch@in.tum.de> / hgweb
- metadata and sitegen for Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Balog_Szemeredi_Gowers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned check names; — Fabian Huch <huch@in.tum.de> / hgweb
- make check roots tool less dependent on AFP structure; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- web for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
- sitegen for Combinatorial_Enumeration_Algorithms — nipkow / hgweb
- New entry Combinatorial_Enumeration_Algorithms — nipkow / hgweb
- fix duplicate affiliations from author and notify; — Fabian Huch <huch@in.tum.de> / hgweb
- add metadata check tool to sitegen; — Fabian Huch <huch@in.tum.de> / hgweb
- update check tools: add formatting checks, new cmd options; — Fabian Huch <huch@in.tum.de> / hgweb
- check for entries instead of session due to session nesting allowed in entries; — Fabian Huch <huch@in.tum.de> / hgweb
- added unused thy check; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified check roots tool; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: encode new notify addresses properly; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: correct build status on empty file; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: remove padding on select; — Fabian Huch <huch@in.tum.de> / hgweb
- re-format metadata; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: update on correct status change; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: clarified date format, tuned logging; — Fabian Huch <huch@in.tum.de> / hgweb
- switch fonts to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
- switch to www prefixed isa-afp.org domain; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp-submit error handling; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp-submit creation and message; — Fabian Huch <huch@in.tum.de> / hgweb
- list submission system website; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: clarified api urls; — Fabian Huch <huch@in.tum.de> / hgweb
- Removal of more unused material — paulson <lp15@cam.ac.uk> / hgweb
- Small simplifications. Removed a needless assumption. — paulson <lp15@cam.ac.uk> / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- more accurate root.bib, based on original \bibitem entries in root.tex 1a42ddd5dbbc; — wenzelm / hgweb
- Fixed the bib issues and supplied a root.bib based on the one in Types_Tableaus_and_Goedels_God (by the same author) — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Added the missing .bib file — paulson <lp15@cam.ac.uk> / hgweb
- proper bib context for formal citations, although there is no document; — wenzelm / hgweb
- back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
- back to unchecked \cite: entry lacks .bib file; — wenzelm / hgweb
- back to unchecked \cite: there is entry lacks .bib file; — wenzelm / hgweb
- proper citation; — wenzelm / hgweb
- merged — desharna / hgweb
- added lemmas image_grounding_of_cls_grounding_of_cls and grounding_of_clss_grounding_of_clss[simp] — desharna / hgweb
- merged — wenzelm / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- merged — Lars Hupel <lars.hupel@mytum.de> / hgweb
- consistent casing in \cite — Lars Hupel <lars.hupel@mytum.de> / hgweb
- ETTS: updated bibliography and citations — user9716869 <user9716869@gmail.com> / hgweb
- merged — wenzelm / hgweb
- more correct and complete citations; — wenzelm / hgweb
- unchecked \cite for unidentifiable citation; — wenzelm / hgweb
- proper @{cite} syntax; — wenzelm / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- Updating Risk Free Lending Entry
- Adding lemma for transfers in special case
- Fixing grammar in abstract
- Adding citation — Matthew Doty <matt@w-d.org> / hgweb - added bibliography to ROOT; — Fabian Huch <huch@in.tum.de> / hgweb
- CTR and ETTS: several amendments (fact names, printing, presentation) — user9716869 <user9716869@gmail.com> / hgweb
- Removed a reference to the (redundant) wf_restr — paulson <lp15@cam.ac.uk> / hgweb
- added bibliographies to ROOTs; — Fabian Huch <huch@in.tum.de> / hgweb
- Changes for generalised lemmas — Katharina Kreuzer / hgweb
- Changes for generalised lemmas — Katharina Kreuzer / hgweb
- Generalised Lemmas — Katharina Kreuzer / hgweb
- merged — desharna / hgweb
- adapted to Isabelle/c9e091867206 — desharna / hgweb
- tuned; — wenzelm / hgweb
- tuned signature, following Isabelle/947510ce4e36; — wenzelm / hgweb
- adapted to Isabelle/25900fbea7ad;
fewer clones of Isabelle sources; — wenzelm / hgweb - adapted to Isabelle/b61ad889dffa — desharna / hgweb
- removed Restricted_Predicates.transp_on following the introduction of equivalent Relation.transp_on in HOL — desharna / hgweb
- merged — desharna / hgweb
- adapted to Isabelle/d33fc5228aae — desharna / hgweb
- fixed proof following Isabelle/66cae055ac7b — desharna / hgweb
- merge — blanchet / hgweb
- adapted to Isabelle/c48fe2be847f — blanchet / hgweb
- enable -no-pie for CakeML — Lars Hupel <lars.hupel@mytum.de> / hgweb
- fixed proofs and removed duplicates following Isabelle/e65a50f6c2de — desharna / hgweb
- tuned proofs to use asymI, asymD, asympI, and asympD — desharna / hgweb
- Fix failing continuous integration — desharna / hgweb
- fixed proof following Isabelle/8fff4e4d81cb — desharna / hgweb
- removed Restricted_Predicates.antisymp_on following the introduction of equivalent Relation.antisymp_on in HOL — desharna / hgweb
- added lemma imgu_range_vars_subset — desharna / hgweb
- Update headers and metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fix ROOT again — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fix ROOT — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Use transfinite induction to prove Lindenbaum's lemma, removing the countable assumption. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fixed proofs following Isabelle/a7d2a7a737b8 — desharna / hgweb
- added lemmas mem_range_varsI and imgu_subst_domain_subset — desharna / hgweb
- weakened the definition of redundant_inference — desharna / hgweb
- removed Restricted_Predicates.irreflp_on following the introduction of equivalent Relation.irreflp_on in HOL — desharna / hgweb
- fixed Containers following introduction of irrefl_on — desharna / hgweb
- added lemmas ex_unify_if_unifiers_not_empty, ex_mgu_if_unifiers_not_empty, and imgu_range_vars_of_equations_vars_subset — desharna / hgweb
- name change — nipkow / hgweb
- AFP and DBLP — nipkow / hgweb
- merged — desharna / hgweb
- added lemmas subst_range_rename_subst_domain_subset and range_vars_rename_subst_domain_subset — desharna / hgweb
- added lemma subst_domain_rename_subst_domain_subset — desharna / hgweb
- added lemma image_the_Var_image_subst_renaming_eq — desharna / hgweb
- Added acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
- Added code export to ROOT — mohammadabdulaziz / hgweb
- Removed out of place code — mohammadabdulaziz / hgweb
- tuned lemma subst_domain_restrict_subst_domain — desharna / hgweb
- added lemmas rename_subst_domain_range_Var_lhs[simp] and rename_subst_domain_range_Var_rhs[simp] — desharna / hgweb
- added attribute [simp] to lemma rename_subst_domain_Var_rhs — desharna / hgweb
- added lemmas inj_on_Var[simp] and rename_subst_domain_Var_lhs[simp] — desharna / hgweb
- merged — desharna / hgweb
- removed Restricted_Predicates.reflp_on following the introduction of equivalent Relation.reflp_on in HOL — desharna / hgweb
- removed Restricted_Predicates.total_on following the introduction of equivalent Relation.totalp_on in HOL — desharna / hgweb
- added lemmas grounding_of_subst_cls_renaming_ident[simp] and grounding_of_subst_clss_renaming_ident[simp] — desharna / hgweb
- added lemmas is_ground_cls_add_mset[simp], grounding_of_subst_cls_subset, and grounding_of_subst_clss_subset — desharna / hgweb
- Streamlined a proof — paulson <lp15@cam.ac.uk> / hgweb
- added lemmas — desharna / hgweb
- moved lemma around — desharna / hgweb
- redefined mgu as a definition — desharna / hgweb
- tuned naming — desharna / hgweb
- fixed proof — desharna / hgweb
- added definition restrict_subst_domain and associated lemmas — desharna / hgweb
- tuned (sub)subsection — desharna / hgweb
- added lemma member_image_the_Var_image_subst — desharna / hgweb
- added lemmas unify_subst_domain_range_vars_disjoint — desharna / hgweb
- added lemma unify_range_vars — desharna / hgweb
- added lemma unify_subst_domain — desharna / hgweb
- added definition rename_subst_domain_range and related lemmas — desharna / hgweb
- merged — desharna / hgweb
- added lemmas vars_term_subst_apply_term and vars_term_subst_apply_term_subset — desharna / hgweb
- Fixed the ROOT file, so that the theory of cardinals is loaded — paulson <lp15@cam.ac.uk> / hgweb
- added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term — desharna / hgweb
- added lemmas unify_append_prefix_same, unify_Cons_same, unify_same, and mgu_same — desharna / hgweb
- added lemma decompose_same_Fun[simp] — desharna / hgweb
- added lemma zip_option_same[simp] — desharna / hgweb
- added definition rename_subst_domain and lemma renaming_cancels_rename_subst_domain — desharna / hgweb
- removed simp annotation from subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
- used rho for renamming — desharna / hgweb
- tuned assumptions — desharna / hgweb
- added lemma subst_apply_term_eq_subst_apply_term_if_mgu — desharna / hgweb
- added lemmas inv_renaming_sound and ex_inverse_of_renaming — desharna / hgweb
- added lemma subst_apply_term_ident — desharna / hgweb
- added lemmas subst_range_Var and range_vars_Var and moved stuff around — desharna / hgweb
- added lemma subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs and tuned naming — desharna / hgweb
- tuned naming — desharna / hgweb
- added lemma mgu_range_vars — desharna / hgweb
- added lemma subst_compose_apply_eq_apply_lhs_if — desharna / hgweb
- added lemmas is_Var_mgu_if_not_in_equations, ball_is_Var_mgu, and inj_on_mgu — desharna / hgweb
- RealTimeDeque: replace `reverseN` with `take_rev — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- replaced Open_Induction.Restricted_Predicates.total_on by equivalent HOL.Relation.totap_on — desharna / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add missing thy files in Sturm_Tarski + repair — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- afp-submit: style page, improve elements; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: added repository updates; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: added download and faster file handling; — Fabian Huch <huch@in.tum.de> / hgweb
- add submission pages to web ui; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: add submission and build status with adapter to existing system; — Fabian Huch <huch@in.tum.de> / hgweb
- add user-facing exception handling to web app; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified submission handling; — Fabian Huch <huch@in.tum.de> / hgweb
- afp-submit: added submission read-only and list views; — Fabian Huch <huch@in.tum.de> / hgweb
- add afp-submit web app; — Fabian Huch <huch@in.tum.de> / hgweb
- add web app facilities; — Fabian Huch <huch@in.tum.de> / hgweb
- RealTimeDeque: Separate implementation and auxiliary functions — Balazs Toth <balazs.toth@quickbirdstudios.com> / hgweb
- Backed out changeset 3a67df508397
The finite simproc is no longer active by default — nipkow / hgweb - adapted to new simproc finite — nipkow / hgweb
- clarified signature, following Isabelle/f362975e8ba1; — wenzelm / hgweb
- more direct Proof_Context.init_global; — wenzelm / hgweb
- proper naming conventions for Isabelle/ML; — wenzelm / hgweb
- Updated citation — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
- merge from afp-2022 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Isabelle2022: new release download links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added tag Isabelle2022 for changeset 548e384c0445 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- import 2022 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- entry names not restricted to alpha-numeric — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- add 2021-1 all releases; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified docs — Fabian Huch <huch@in.tum.de> / hgweb
- replace old get-releases tool (now isabelle afp_release -I); — Fabian Huch <huch@in.tum.de> / hgweb
- add option for parallel session builds — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- set Isabelle2022 release date — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- set release version to 2022 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- merge from afp-2021-1 — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- Removal of some old junk — paulson <lp15@cam.ac.uk> / hgweb
- Deleted unused material — paulson <lp15@cam.ac.uk> / hgweb
- nothing — paulson <lp15@cam.ac.uk> / hgweb
- Instantiation of the order solver for ⊑ and ⊏ (no real effect though) — paulson <lp15@cam.ac.uk> / hgweb
- proof simplifications — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Simplified the proofs a bit — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- replaced fmember.rep_eq by fmember_iff_member_fset — desharna / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- only make parent dir; — Fabian Huch <huch@in.tum.de> / hgweb
- accept all dois; — Fabian Huch <huch@in.tum.de> / hgweb
- metadata toml: tuned error messages; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified sub topics; — Fabian Huch <huch@in.tum.de> / hgweb
- adapted to Isabelle/457f1cba78fb — desharna / hgweb
- merged — desharna / hgweb
- added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;
added simp annotation to generalizes_refl — desharna / hgweb - extracted proof cases from lifting_lemma to distinct lemmas — desharna / hgweb
- tuned proof due to new simp rules — nipkow / hgweb
- corresponding lemma was removed from distribution — nipkow / hgweb
- regen site — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- updates to BenOr_Kozen_Reif by Katherine Kosaian — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix author entry; regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add change history revision — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added scene spaces, improvements to prisms, and improvements to the alphabet command. — Simon Foster <simon.foster@york.ac.uk> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Query_Optimization — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- remove temp file — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Complex_Bounded_Operators: Various changes:
- Removed auxiliary constant `the_riesz_rep_bilinear'`
- Renamed constant `the_riesz_rep_bilinear` -> `the_riesz_rep_sesqui` and defined differently but equivalently
- Renamed constant `bifunctional` -> `bidual_embedding`
(and renamed lemmas containing `bifunctional` accordingly)
- Renamed lemmas `the_riesz_rep_bilinear_apply` -> `the_riesz_rep_sesqui_apply`,
`cblinfun_extension_exists_norm` -> `cblinfun_extension_norm_bounded_dense`
- New theorems: `rank1_compose_left`, `rank1_compose_right`, `rank1_scaleC`,
`rank1_uminus`, `rank1_uminus_iff`, `rank1_adj`, `rank1_adj_iff`,
`bidual_embedding_surj`, `Cblinfun_comp_bounded_cbilinear`, `Cblinfun_comp_bounded_sesquilinear`, `bounded_clinear_0`,
`bounded_antilinear_0`, `bounded_cbilinear_0`, `bounded_sesquilinear_0`, `bounded_cbilinear_apply_bounded_clinear`,
`bounded_sesquilinear_apply_bounded_clinear`, `cblinfun_extension_exists_hilbert`, `trunc_ell2_reduces_norm`,
`trunc_ell2_add`, `trunc_ell2_scaleC`, `bounded_clinear_trunc_ell2`
- Theorem `cblinfun_extension_exists_proj`: Reformulated one assumption — Gerwin Klein <kleing@unsw.edu.au> / hgweb - slightly less abusive proof pattern — haftmann / hgweb
- Many changes to entry `Complex_Bounded_Operators`:
- Removed all use of deprecated `⟨.,.⟩` syntax for complex inner product. (Now: `∙⇩C`)
- Cosmetic changes and cleanup of some proofs
- Type class `one_dim` inherits from `complex_inner` now.
- Moved various theorems around between theories
- Added `[simp]` to: `Proj_partial_isometry`, `cadjoint_id`
- Removed theorems: `onorm_Inf_bound`, `norm_unit_sphere`
- Changed theorems: `of_complex_cblinfun_apply` (made into more general simp-rule), TODO orthospacething
- New definition: `rank1` (and lemmas about it)
- New theorems: `one_dim_iso_cblinfun_apply`, `vector_to_cblinfun_one_dim_iso`, `image_vector_to_cblinfun_adj`,
`image_vector_to_cblinfun_adj'`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`,
`one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary`
- Renamed `vector_to_cblinfun_cblinfun_apply` -> `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`),
`cancel_apply_Proj` -> `Proj_fixes_image`, `range_is_clinear` -> `range_is_csubspace`.
- Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`)
Fixed entry `Registers` due to the changes above. — Dominique Unruh <unruh@ut.ee> / hgweb - tuned proofs — haftmann / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Undirected_Graph_Theory — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- typo — nipkow / hgweb
- typo — nipkow / hgweb
- New entry: Maximum_Segment_Sum — nipkow / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- added topic for data management systems; — Fabian Huch <huch@in.tum.de> / hgweb
- added missing file — nipkow / hgweb
- New entry Safe_Range_RC — nipkow / hgweb
- adjust Stalnaker_Logic to changes in Epistemic_Logic; — Fabian Huch <huch@in.tum.de> / hgweb
- adjusted to distribution — haftmann / hgweb
- remove duplicate code; — Fabian Huch <huch@in.tum.de> / hgweb
- restructure afp ci builds (see Isabelle/3c4e373922ca) — Fabian Huch <huch@in.tum.de> / hgweb
- Cosmetic changes. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- afp site: minor stylistic improvements; — Fabian Huch <huch@in.tum.de> / hgweb
- web entry for Stalnaker_Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Stalnaker Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- clarified options, following f2094906e491; — wenzelm / hgweb
- Comments on theories brought from ZF-Constructible. Shortening fm names — sterraf / hgweb
- adjusted to distribution — haftmann / hgweb
- Remove fontenc from root.tex to make Ł show in PDF. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Update ROOT... — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Appendix with another axiom system as a variant of the proof. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- adapt to Isabelle@769a7cd5a16a — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust Lar's contact info as requested — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sitegen for Padic_Field — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry: Padic_Field — Manuel Eberl <manuel@pruvisto.org> / hgweb
- sitegen for Risk_Free_Lending — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry: Risk_Free_Lending — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry Implicational_Logic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry Separation_Logic_Unbounded — nipkow / hgweb
- added web files — nipkow / hgweb
- added web files — nipkow / hgweb
- New entry SCC_Bloemen_Sequential — nipkow / hgweb
- A few more disambiguations, related to locales in CartesianCategory. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Merged — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Further disambiguation of facts to address clashes involving ConcreteCategory as a sublocale. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- streamlined division on polynomials — haftmann / hgweb
- Complex_Bounded_Operators: Fixed errors in document generation — Dominique Unruh <unruh@ut.ee> / hgweb
- Complex_Bounded_Operators: Added numerous new lemmas. — Dominique Unruh <unruh@ut.ee> / hgweb
- Merged — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Disambiguate sufficiently many facts in locales so as to permit a top-level interpretation of ZFC_set_cat. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Fix a typo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Neater links — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Relational_Disjoint_Set_Forests: variant abstraction — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- merged — wenzelm / hgweb
- support for ISABELLE_MLTON_OPTIONS, following Isabelle/d27ed188e0c4; — wenzelm / hgweb
- Renaming synthesized formulas — sterraf / hgweb
- prefer (smt (verit)), which is potentially more stable under heavy load; — wenzelm / hgweb
- Add additional results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Formatting. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add papers to abstracts. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merged — paulson / hgweb
- Purely cosmetic — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Deleted one redundant step — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Merge — paulson <lp15@cam.ac.uk> / hgweb
- Tidied (a lot) — paulson <lp15@cam.ac.uk> / hgweb
- added missing congruence rule — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- streamlined — haftmann / hgweb
- tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- merged — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- some slight polishing in the UTM entry — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added congruence rule for forallM of Error-Monad — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- updated to devel — nipkow / hgweb
- merged — wenzelm / hgweb
- tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load; — wenzelm / hgweb
- removed obsolete workaround (see Isabelle/91ee232b4211); — wenzelm / hgweb
- Eliminated the temporary material that was already migrated to the Isabelle libraries — paulson <lp15@cam.ac.uk> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- merged — paulson / hgweb
- New entry CRYSTALS-Kyber — paulson <lp15@cam.ac.uk> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- added missing history in metadata; — Fabian Huch <huch@in.tum.de> / hgweb
- retrieve missing change history in metadata migration tool; — Fabian Huch <huch@in.tum.de> / hgweb
- backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726 — Fabian Huch <huch@in.tum.de> / hgweb
- new email address for Maksym — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata and sitegen for Khovansikii_Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Khovanski-Theorem — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- fixed metadata for Hales_Jewett — Manuel Eberl <manuel@pruvisto.org> / hgweb
- sitegen for Number_Theoretic_Transform — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry Number_Theoretic_Transform — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry Hales Jewett — nipkow / hgweb
- adapt to only check ROOT for directories in thys (aftermath of Isabelle/a9bbf075f4319e920a22a1c0a5b763b6575f2089); — Fabian Huch <huch@in.tum.de> / hgweb
- updated entry for Universal Turing Machines — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- merged — desharna / hgweb
- adapted to antimono — desharna / hgweb
- merged — desharna / hgweb
- adapted to new mono and strict_mono — desharna / hgweb
- updated to Isabelle/5ea588440b06 — desharna / hgweb
- Updated citations — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
- Updated citations — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
- tuned signature; — wenzelm / hgweb
- merged — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- Substantial additions by Franz Regensburger to the Universal_Turing_Machine entry — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- tuned timeouts, based on test runs with threads=1; — wenzelm / hgweb
- replaced slow smt call by blast — blanchet / hgweb
- avoid hardwired document; — wenzelm / hgweb
- merged — paulson / hgweb
- cosmetic — paulson <lp15@cam.ac.uk> / hgweb
- replace smt_oracle by proper veriT reconstruction — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
- merged — paulson / hgweb
- tweaks — paulson <lp15@cam.ac.uk> / hgweb
- make all sessions of chapter "AFP" belong to group "AFP"; — wenzelm / hgweb
- chapter_definition for presentation; — wenzelm / hgweb
- Undo an unrelated change that somehow crept into the previous commit. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Remove lots of unnecessary explicit quantifiers in lemma statements, now that I've discovered "arbitrary:". — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Revised locale structure and notation. Proposed modularization for ZF-Constructible's M_eclose — sterraf / hgweb
- tuning — blanchet / hgweb
- updated entries: Combinatorics_Words, Combinatorics_Words_Lyndon, and Combinatorics_Words_Graph_Lemma — Štěpán Starosta <stepan.starosta@fit.cvut.cz> / hgweb
- avoid fact name clash — haftmann / hgweb
- adjusted to distribution — haftmann / hgweb
- repaired proof — haftmann / hgweb
- Complex_Bounded_Operators: Fixed document generation — Dominique Unruh <unruh@ut.ee> / hgweb
- Merged changes. — Dominique Unruh <unruh@ut.ee> / hgweb
- Registers: Fixed parse error. — Dominique Unruh <unruh@ut.ee> / hgweb
- Misc updates to Complex_Bounded_Operators:
Many new lemmas.
New definitions: cblinfun_power, cblinfun_left, cblinfun_right, ccsubspace_Times, partial_isometry, the_riesz_rep, the_riesz_rep_bilinear', the_riesz_rep_bilinear, bij_between_bases, unitary_between, is_onb, some_chilbert_basis, rel_ccsubspace.
instance prod :: complex_normed_vector.
Changed infix priority of oCL to 67.
Changed local structure: Complex locales now are sublocales of real locals with prefix real.
Renamed norm_blinfun_id_le -> norm_cblinfun_id_le. — Dominique Unruh <unruh@ut.ee> / hgweb - Reintroduce type signatures. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Switch to simultaneous substitutions. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry: Nano_JSON — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sitegen for Commuting_Hermitian — Manuel Eberl <manuel@pruvisto.org> / hgweb
- new entry: Commuting_Hermitian — Manuel Eberl <manuel@pruvisto.org> / hgweb
- Sitegen for Involutions2Squares (WITH WRONG EMAIL ADDRESS) — paulson <lp15@cam.ac.uk> / hgweb
- new entry Involutions2Squares — paulson <lp15@cam.ac.uk> / hgweb
- fix typo — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Solidity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- tuned title — nipkow / hgweb
- more typos — nipkow / hgweb
- regenerate because of typos — nipkow / hgweb
- New entry — nipkow / hgweb
- topics no longer exist — nipkow / hgweb
- new topics — nipkow / hgweb
- New entry FSM_Tests — nipkow / hgweb
- merged — wenzelm / hgweb
- Isabelle/b6589c8ccadd officially supports README.thy; — wenzelm / hgweb
- streamlined — haftmann / hgweb
- tuned proofs — haftmann / hgweb
- discontinued obsolete README.html: superseded by abstract provided by AFP; — wenzelm / hgweb
- streamlined primitive definitions for integer division — haftmann / hgweb
- tuned code equations for Xml-parsing — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- refactored algebraic number theories, generalized Cauchy Root Bounds lemma (so that real and complex numbers work) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Revision of locale structure — sterraf / hgweb
- Purely markup — paulson <lp15@cam.ac.uk> / hgweb
- Fix ImpSplit thy for document generation — Niels Mündler <n.muendler@web.de> / hgweb
- Add B+Tree formalisation to the BTree entry — Niels Mündler <n.muendler@web.de> / hgweb
- Correcting thm antiquotations. Turning code comments into text — sterraf / hgweb
- Update metadata and root.tex to mention the addition of ZFC_SetCat in early 2022. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Sync with my development repo: Category3: add various rules for limits. RTS: strengthen definition of transformation. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- adapted to NLists.thy — nipkow / hgweb
- merged — nipkow / hgweb
- use Library/NList.thy now — nipkow / hgweb
- Further streamlining of quick-and-dirty evaluation. — haftmann / hgweb
- An attempt for an integrated solution for quick-and-dirty evaluation. — haftmann / hgweb
- Further reduction of locale assumptions — sterraf / hgweb
- merged — wenzelm / hgweb
- more complete theorem_commands; — wenzelm / hgweb
- clarified signature, following Isabelle/b6d74c90b588; — wenzelm / hgweb
- Update metadata for Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
- merged — Richard Schmoetten <richard.schmoetten@ed.ac.uk> / hgweb
- Update Schutz_Spacetime
chain (and other) definitions, notations, extra gorder proof, general cleanup
corresponds to revisions to JAR paper — Richard Schmoetten <richard.schmoetten@ed.ac.uk> / hgweb - more accurate name — blanchet / hgweb
- more politically correct — blanchet / hgweb
- two new lemmas — paulson <lp15@cam.ac.uk> / hgweb
- added two lemmas to relational chains — blanchet / hgweb
- changed confusing assumption name — blanchet / hgweb
- avoid the surprise that n-m is 0 even if n<m. — nipkow / hgweb
- tuned — nipkow / hgweb
- simplified invar — nipkow / hgweb
- merged — nipkow / hgweb
- simplified — nipkow / hgweb
- update metadata; — wenzelm / hgweb
- merged — nipkow / hgweb
- tuned — nipkow / hgweb
- removed a spurious locale parameter -- the same issue probably arises in the pen-and-paper Waldmann et al. — blanchet / hgweb
- removed needless assumption — blanchet / hgweb
- Named intermediate results combinable wands — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
- Named intermediate results Package logic — Thibault Dardinier <thibault.dardinier@inf.ethz.ch> / hgweb
- added lemma about lazy list chains — blanchet / hgweb
- typo — blanchet / hgweb
- Refining three sessions.
* Delta_System_Lemma: Moving results out of the scope of AC.
* Transitive_Models: General locale re-engineering.
* Independence_CH: specifying finite set of axioms required for
forcing CH and ¬CH. — sterraf / hgweb - Tuned. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merged — nipkow / hgweb
- addd DOIs and other metadata links — nipkow / hgweb
- some slight polishing of the definitions — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added links — nipkow / hgweb
- added metadata links — nipkow / hgweb
- added link — nipkow / hgweb
- added Wiki link — nipkow / hgweb
- added DOIs — nipkow / hgweb
- added DIs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- Added DOIs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- merged — nipkow / hgweb
- added DOIs — nipkow / hgweb
- XZ compression for Safe_Distance examples (safes 160 MB!) — Manuel Eberl <eberlm@in.tum.de> / hgweb
- tuned DOIs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- added pubs — nipkow / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- improve DOI resolving: offline cache and better timeouts; — Fabian Huch <huch@in.tum.de> / hgweb
- added pubs — nipkow / hgweb
- added DOIs — nipkow / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- resolve DOIs in sitegen to formatted citations; — Fabian Huch <huch@in.tum.de> / hgweb
- removed links from related references; — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- Remove duplication between Universal_Hash_Families (UHF) and Finite_Fields (FF).
- Also remove white space in UHF. — Emin Karayel <me@eminkarayel.de> / hgweb - Update metadata for WOOT_Strong_Eventual_Consistency.
- Added corresponding publication in related works.
- Added orcid id's of authors. — Emin Karayel <me@eminkarayel.de> / hgweb - added DOI — nipkow / hgweb
- added DOI — nipkow / hgweb
- merged — nipkow / hgweb
- added orcid — nipkow / hgweb
- added orcid — nipkow / hgweb
- added lemma — nipkow / hgweb
- ORCID for Manuel Eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- updated help page; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified doc; — Fabian Huch <huch@in.tum.de> / hgweb
- name change for Kądziołka — Manuel Eberl <manuel@pruvisto.org> / hgweb
- updated docs on metadata; — Fabian Huch <huch@in.tum.de> / hgweb
- adjusted topics and added subject classifications; — Fabian Huch <huch@in.tum.de> / hgweb
- name change for Kądziołka — Manuel Eberl <manuel@pruvisto.org> / hgweb
- moved lemma to distribution — nipkow / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- added more metadata fields: related references for entries, orcids for authors, and acm/ams subject classification for topics; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned topics — nipkow / hgweb
- adjusted topics — nipkow / hgweb
- proper license link; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen: integrate change history and note properly; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified homepage urls; — Fabian Huch <huch@in.tum.de> / hgweb
- remove metadata migration tool; — Fabian Huch <huch@in.tum.de> / hgweb
- toml parser improvements: comments are now treated as whitespace. — Fabian Huch <huch@in.tum.de> / hgweb
- clarified metadata loading and added more metadata checks; — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- improve releases view and map correctly to Isabelle version; — Fabian Huch <huch@in.tum.de> / hgweb
- add missing releases again; — Fabian Huch <huch@in.tum.de> / hgweb
- merged — paulson / hgweb
- sitegen for Weighted_Arithmetic_Geometric_Mean — paulson <lp15@cam.ac.uk> / hgweb
- new entry Weighted_Arithmetic_Geometric_Mean — paulson <lp15@cam.ac.uk> / hgweb
- missing file — nipkow / hgweb
- New entry IMP_Compiler_Reuse — nipkow / hgweb
- Just variable renamings — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Simplified and shortened some proofs — paulson <lp15@cam.ac.uk> / hgweb
- moved lemmas to distribution — nipkow / hgweb
- merged — paulson / hgweb
- tweaked — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- a bit of tidying — paulson <lp15@cam.ac.uk> / hgweb
- cleanup with global-interpretations and code equations in Simplex_Incremental — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- changed incremental simplex interface: check now always returns a new state, even in unsat-case — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- Improvements. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen: tuned statistics; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- sitegen for Boolos_Curious_Inference — paulson <lp15@cam.ac.uk> / hgweb
- new entry: Boolos_Curious_Inference — paulson <lp15@cam.ac.uk> / hgweb
- website: proper bibtex entries; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned — haftmann / hgweb
- removed more material now residing in distribution — haftmann / hgweb
- separated non-computable instance of bit comprehension from computable one — haftmann / hgweb
- Small changes. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Undo accidental changes. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Tuned. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- tuned -- follow clone in $ISABELLE_HOME/src/HOL/Imperative_HOL/Heap_Monad.thy; — wenzelm / hgweb
- minor performance tuning: avoid redundant BigInt construction; — wenzelm / hgweb
- prefer self-made Array.T, to avoid problems with ArraySeq in Scala 3; — wenzelm / hgweb
- more robust Array.T for Scala 2.13 and 3.x, following Isabelle/ca450d902198; — wenzelm / hgweb
- Move code lemmas for symbolic computation of bit operations on int to distribution. — haftmann / hgweb
- renamings — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Relational_Disjoint_Set_Forests: improved abstractions — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- Simplified a proof using Cauchy–Schwarz — paulson <lp15@cam.ac.uk> / hgweb
- removed precondition in det_four_block_mat — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- removed assumption in det_bound_hadamard_tight, moved some basic lemmas on matrices, added a conditional version of det(four_block_mat ...) = ... — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- updated doc; — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate site; — Fabian Huch <huch@in.tum.de> / hgweb
- obfuscate email addresses in metadata and generated site; — Fabian Huch <huch@in.tum.de> / hgweb
- renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using unproven fact about determinants of block-matrices) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added lemma for special case of small integer solutions (no mixed integer), where then everything is of type int — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- document change in metadata — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- generalized fixed bounds on determinants to predicate; added an improved determinate bound
-> result: get smaller bound on mixed integer solutions (replace n! by sqrt(n^n)) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb - Code generated in the same directory — mohammadabdulaziz / hgweb
- Removed ML code from AFP entry — mohammadabdulaziz / hgweb
- adapted to scala-3.1.2; — wenzelm / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tooling: added utility to check for metadata consistency; — Fabian Huch <huch@in.tum.de> / hgweb
- regenerate website; — Fabian Huch <huch@in.tum.de> / hgweb
- site: generate multi-line json for smaller merges; — Fabian Huch <huch@in.tum.de> / hgweb
- toml module: proper parsing of quotes in multiline strings; — Fabian Huch <huch@in.tum.de> / hgweb
- added further sitegen generated websites — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added metadata for Real_Time_Deque's, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Real-Time Double-Ended Queue — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merged — desharna / hgweb
- replaced IMGU by min_IMGU — desharna / hgweb
- replaced MGU by IMGU — desharna / hgweb
- exposed that inverse of renaming only maps variables to variables — desharna / hgweb
- added the r{n..} regular expression to the extensions directory in the Posix-Lexing entry, added two small lemmas to the Regular-Set theory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- regenerate website — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- do not ignore admin/site — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- remove afp python component build tool; — Fabian Huch <huch@in.tum.de> / hgweb
- afp tooling: improve keyword extraction; — Fabian Huch <huch@in.tum.de> / hgweb
- website: small improvements; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned efficiency of XML parser — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- updated the abstract in root.tex — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- added the r{..n} regular expression to the extensions directory — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- merged — traytel / hgweb
- tuned BNF bound — traytel / hgweb
- strict bounds for BNFs (by Jan van Brügge) — traytel / hgweb
- merge from afp-2021-1 (replaying devel commit) — Fabian Huch <huch@in.tum.de> / hgweb
- replaced python RAKE component with Isabelle/Scala Rake component; — Fabian Huch <huch@in.tum.de> / hgweb
- remove scala tools from publish; — Fabian Huch <huch@in.tum.de> / hgweb
- replaced python RAKE component with Isabelle/Scala Rake component; — Fabian Huch <huch@in.tum.de> / hgweb
- merged — wenzelm / hgweb
- avoid hardwired pdf; — wenzelm / hgweb
- adapted to Isabelle/986506233812; — wenzelm / hgweb
- merged — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- added an implementation of pseudo remainder sequences for calculating Tarski queries — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- merged — desharna / hgweb
- updated to Isabelle/3c544d64c218 — desharna / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- tuned error messages; — Fabian Huch <huch@in.tum.de> / hgweb
- mention error location when metadata loading fails; — Fabian Huch <huch@in.tum.de> / hgweb
- merged — Fabian Huch <huch@in.tum.de> / hgweb
- even more IsaNet; — Fabian Huch <huch@in.tum.de> / hgweb
- afp metadata/releases: change format to re-add releases swallowed by key-set, remove extra releases; — Fabian Huch <huch@in.tum.de> / hgweb
- more IsaNet — nipkow / hgweb
- New entry IsaNet — nipkow / hgweb
- adapted to Isabelle/39df30349778; — wenzelm / hgweb
- added extension that deals with the n-times regular expression in Posix-Lexing — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- Avoid calculations where not necessary. — haftmann / hgweb
- used long version of definition to avoid conflict when introducing HOL.monotone_on — desharna / hgweb
- merge from afp-2021-1 (metadata consolidation) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sitegen — nipkow / hgweb
- unified home pages — nipkow / hgweb
- re-introduce accidentally reverted changes — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- ignore dev site output — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- consolidate metadata (email and homepages) — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- load mail configuration lazily (initialized later from properties); — Fabian Huch <huch@in.tum.de> / hgweb
- tuned home pages — nipkow / hgweb
- merge from afp-2021-1 — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- proper topics loading; — Fabian Huch <huch@in.tum.de> / hgweb
- merge from afp-2021-1 (new website) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new website — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- admin: remove old sitegen lib files — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- update metadata to new sitegen — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- merge website-redesign graft — Gerwin Klein <gerwin.klein@proofcraft.systems> / hgweb
- updated afp sitegen doc; — Fabian Huch <huch@in.tum.de> / hgweb
- replaced python afp stats with Isabelle/Scala tool; — Fabian Huch <huch@in.tum.de> / hgweb
- updated afp metadata doc (now as markdown); — Fabian Huch <huch@in.tum.de> / hgweb
- afp components: removed unnecessary platforms; — Fabian Huch <huch@in.tum.de> / hgweb
- afp sitegen: switch to new version; — Fabian Huch <huch@in.tum.de> / hgweb
- add sitegen ignore option; — Fabian Huch <huch@in.tum.de> / hgweb
- improvements for toml module: proper boolean values; — Fabian Huch <huch@in.tum.de> / hgweb
- add components as proper afp deps; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- switched to standalone cross-platform afp python component; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- afp python build: use tgz for better cross-plattform compatability; — Fabian Huch <huch@in.tum.de> / hgweb
- replaced ci_profiles by statically compiled afp_build tool (Scala 3 preparations); — Fabian Huch <huch@in.tum.de> / hgweb
- afp structure: added accessors; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: minor changes; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo-site: improve various aspects; — Fabian Huch <huch@in.tum.de> / hgweb
- add new authors to migration; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified formatting, for the sake of scala3; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: better scrolling; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: updated devel info; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: updated content; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: proper ordering; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: restricted generated affiliations;
hugo site: added fresh option; — Fabian Huch <huch@in.tum.de> / hgweb - hugo site: proper theory view link scrolling; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: tuned affiliation keys; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: proper topic-only topics page; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: relativize paths; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: list sessions separately; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: merge gen and build tool; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: added doc headers; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- afp metadata: index keys for emails and urls;
apf metadata: separate license file; — Fabian Huch <huch@in.tum.de> / hgweb - hugo site: improve theory view; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: cleaned up; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: added devel version; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: updated search and content; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: added theory view styling for different device sizes;
hugo site: update contributions; — Fabian Huch <huch@in.tum.de> / hgweb - Updated metadata in migration and theory view; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo site: updated site templates; — Fabian Huch <huch@in.tum.de> / hgweb
- metadata migration: updated authors; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo: added mobile view; — Fabian Huch <huch@in.tum.de> / hgweb
- hugo: copy to proper path; — Fabian Huch <huch@in.tum.de> / hgweb
- added theory navbar; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned formatting; — Fabian Huch <huch@in.tum.de> / hgweb
- added loader; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned: more canonical Isabelle code style; — Fabian Huch <huch@in.tum.de> / hgweb
- proper loading of foundational hrefs; — Fabian Huch <huch@in.tum.de> / hgweb
- fix dependencies; — Fabian Huch <huch@in.tum.de> / hgweb
- added devel flag; — Fabian Huch <huch@in.tum.de> / hgweb
- updated about page; — Fabian Huch <huch@in.tum.de> / hgweb
- moved extraction of related entries to hugo; — Fabian Huch <huch@in.tum.de> / hgweb
- improved keyword extraction; — Fabian Huch <huch@in.tum.de> / hgweb
- added keywords to site generated entry data; — Fabian Huch <huch@in.tum.de> / hgweb
- use tmp file for python script instead of command; — Fabian Huch <huch@in.tum.de> / hgweb
- added js-side theory loading to afp site; — Fabian Huch <huch@in.tum.de> / hgweb
- integrated metadata changes into site;
tuned; — Fabian Huch <huch@in.tum.de> / hgweb - added missing keyword data; — Fabian Huch <huch@in.tum.de> / hgweb
- removed html dir from sitegen (now set inside hugo); — Fabian Huch <huch@in.tum.de> / hgweb
- tuned sitegen: moved dependencies generation to scala — Fabian Huch <huch@in.tum.de> / hgweb
- changed generated author format; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned hugo: static files more explicit; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- proper authors/affiliations gen for hugo taxonomy; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified hugo data; — Fabian Huch <huch@in.tum.de> / hgweb
- added missing name mapping to migration; — Fabian Huch <huch@in.tum.de> / hgweb
- proper output path; — Fabian Huch <huch@in.tum.de> / hgweb
- added missing topics; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified hugo build signature;
split site generation into own afp site gen tool; — Fabian Huch <huch@in.tum.de> / hgweb - added more steps to afp site generation tool; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned;
clarified hugo; — Fabian Huch <huch@in.tum.de> / hgweb - added hugo project by Carlin MacKenzie; — Fabian Huch <huch@in.tum.de> / hgweb
- added sitegen scripts by Carlin MacKenzie (slightly tweaked); — Fabian Huch <huch@in.tum.de> / hgweb
- added afp hugo module; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified afp_dependencies: proper typed output;
added afp_dependencies json module; — Fabian Huch <huch@in.tum.de> / hgweb - Added afp structure module; — Fabian Huch <huch@in.tum.de> / hgweb
- Added python wrapper; — Fabian Huch <huch@in.tum.de> / hgweb
- clarified metadata; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- added afp hugo component; — Fabian Huch <huch@in.tum.de> / hgweb
- added afp python component with required packages; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(afp/tools): added initial site build tool — Fabian Huch <huch@in.tum.de> / hgweb
- tuned(afp/tools): metadata sorted — Fabian Huch <huch@in.tum.de> / hgweb
- tuned(afp/tools): tuned parser/unparser — Fabian Huch <huch@in.tum.de> / hgweb
- feat(afp/tools): more metadata and toml conversion; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(afp/tools): added TOML lexer and parser; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned(afp/tools): module jar locations; — Fabian Huch <huch@in.tum.de> / hgweb
- fix(afp/tools): added missing metadata, improved toml structure — Fabian Huch <huch@in.tum.de> / hgweb
- fix(afp/tools): removed TOML formatting heuristics for simplicity; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(afp/tools): added TOML module; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(afp/tools): added metadata migration tool; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(afp/tools): migrated scala tool_bodys to proper tools; — Fabian Huch <huch@in.tum.de> / hgweb
- Avoid explicit operation when not necessary. — haftmann / hgweb
- adjust for isabelle@5bba3516ddb5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added a missing acknowledgement — paulson <lp15@cam.ac.uk> / hgweb
- metadata for Finite_Fields (and missing <> for two previous entries) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Finite_Fields — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for DPRM_Theorem — paulson <lp15@cam.ac.uk> / hgweb
- DPRM_Theorem: finally cleaned up and impressive! — paulson <lp15@cam.ac.uk> / hgweb
- New entry [Rewrite_Properties_Reduction] — nipkow / hgweb
- Fixed broken LaTeX in the abstract — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Combinable_Wands — paulson <lp15@cam.ac.uk> / hgweb
- New entry Combinable_Wands — paulson <lp15@cam.ac.uk> / hgweb
- corrected metadata (separate authors by "," not by "and") — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen and metadata for Pluennecke_Ruzsa_Inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Pluennecke Ruzsa Inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Tuning the abstract to remove some of the display mathematics — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Package_logic — paulson <lp15@cam.ac.uk> / hgweb
- new entry Package_logic — paulson <lp15@cam.ac.uk> / hgweb
- Removal of all email addresses, at authors' request — paulson <lp15@cam.ac.uk> / hgweb
- renamed some variables — paulson <lp15@cam.ac.uk> / hgweb
- proper \open\close markup — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- Updated the Posix-Lexer entry including a small change in Regular-Set — Christian Urban <christian.urban@kcl.ac.uk> / hgweb
- Trimmed down dependencies. — haftmann / hgweb
- Merge equivalent instance declarations for functions in Lp.Functional_Spaces and HOL-Library.Function_Algebras.
Because of the distinct but equivalent instance declarations in the mentioned theories, it was not possible to import both libraries at the same time.
This commit fixes the problem. — Emin Karayel <me@eminkarayel.de> / hgweb - Remove duplicate lemma and fix typos in Frequency_Moments. — Emin Karayel <me@eminkarayel.de> / hgweb
- same variant as for imperative algorithm to prove n^2 complexity — nipkow / hgweb
- tuned — nipkow / hgweb
- Shortened and simplified a proof — paulson <lp15@cam.ac.uk> / hgweb
- more realistic timeout; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- more realistic timeout;
more parallelism; — wenzelm / hgweb - avoid hard-wired document; — wenzelm / hgweb
- removed usages of HOL.no_atp as its content and order is not guaranteed — desharna / hgweb
- cleaning — nipkow / hgweb
- no separate code-equations required for a lift_definition by using (code_dt) instead — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- The last few occurrences of integrable_cong — paulson <lp15@cam.ac.uk> / hgweb
- Tidying/removal of obsolete material — paulson <lp15@cam.ac.uk> / hgweb
- Fixed a use of Bochner_Integration.integrable_cong — paulson <lp15@cam.ac.uk> / hgweb
- fixes for compatibility with renamed / new lemmas — paulson <lp15@cam.ac.uk> / hgweb
- Tiny simplifications — paulson <lp15@cam.ac.uk> / hgweb
- A tiny bit of reorganisation — paulson <lp15@cam.ac.uk> / hgweb
- the last "simp/auto" problems — paulson <lp15@cam.ac.uk> / hgweb
- corrected all "bysimp" — paulson <lp15@cam.ac.uk> / hgweb
- Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.3gPj1U — paulson <lp15@cam.ac.uk> / hgweb
- Tidied auto/simp with null arguments — paulson <lp15@cam.ac.uk> / hgweb
- merged — nipkow / hgweb
- comleted single loop refinement — nipkow / hgweb
- minor adjustments — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata — user9716869 <user9716869@gmail.com> / hgweb
- minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- creation and preservation of limits; a variety of auxiliary results and amendments — user9716869 <user9716869@gmail.com> / hgweb
- patched a broken proof — paulson <lp15@cam.ac.uk> / hgweb
- merged — nipkow / hgweb
- single lopp variant refined to lists. — nipkow / hgweb
- adjust for isabelle@7095df141819 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- typo fix — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for Digit_Expansions — paulson <lp15@cam.ac.uk> / hgweb
- New entry Digit_Expansions — paulson <lp15@cam.ac.uk> / hgweb
- finally!!!! Sitegen for Sophomore's Dream — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Minor corrections to metadata (no "and" between authors' names) — paulson <lp15@cam.ac.uk> / hgweb
- Updating the version of Jinja2, as suggested by Manuel — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- updated metadata — paulson <lp15@cam.ac.uk> / hgweb
- new entry Sophomores_Dream — paulson <lp15@cam.ac.uk> / hgweb
- updated name and email address of Rose Bohrer — Manuel Eberl <manuel@pruvisto.org> / hgweb
- sitegen for Clique_and_Monotone_Circuits — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Clique_and_Monotone_Circuits — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for Fisher's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Fisher's Inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry Multiset_Ordering_NPC — nipkow / hgweb
- sitegen for Frequence_Moments — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Frequence_Moments — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata and sitegen for Prefix_Free_Code_Combinators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Prefix_Free_Code_Combinators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- regen website (some orders are different in python3) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- switch sitegen to python3 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sitegen for new entry — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: FOL_Seq_Calc3 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry: Dedekind_Real — nipkow / hgweb
- New entry Ackermann_not_PR, from distribution — nipkow / hgweb
- Cotangent_PFD_Formula sitegen — paulson <lp15@cam.ac.uk> / hgweb
- new entry Cotangent_PFD_Formula — paulson <lp15@cam.ac.uk> / hgweb
- website for Independence_CH — paulson <lp15@cam.ac.uk> / hgweb
- new entry Independence_CH — paulson <lp15@cam.ac.uk> / hgweb
- New entry ResiduatedTransitionSystem — nipkow / hgweb
- Transitive_Models webpage — paulson <lp15@cam.ac.uk> / hgweb
- new entry Transitive_Models — paulson <lp15@cam.ac.uk> / hgweb
- updated name and email address of Rose Bohrer — Manuel Eberl <manuel@pruvisto.org> / hgweb
- Removal of unnecessary material — paulson <lp15@cam.ac.uk> / hgweb
- perfectly pointless streamlining — paulson <lp15@cam.ac.uk> / hgweb
- More general definition of gcard — paulson <lp15@cam.ac.uk> / hgweb
- refined one-loop version further — nipkow / hgweb
- tidied up a few proofs — paulson <lp15@cam.ac.uk> / hgweb
- A bit of beautification — paulson <lp15@cam.ac.uk> / hgweb
- Yet more tidying and streamlining of graph lemmas — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- A few trivial changes — paulson <lp15@cam.ac.uk> / hgweb
- Tweaks concerning the versions of Zhao's evolving lecture notes — paulson <lp15@cam.ac.uk> / hgweb
- Trying to simplify a bit more — paulson <lp15@cam.ac.uk> / hgweb
- More simplification of proofs. Removal of numeric references to Zhao. — paulson <lp15@cam.ac.uk> / hgweb
- tidying and simplification — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- More purely cosmetic changes — paulson <lp15@cam.ac.uk> / hgweb
- moved from AFP to distribution — haftmann / hgweb
- tuned syntax — haftmann / hgweb
- simplified some proofs and deleted quite a bit of redundant material — paulson <lp15@cam.ac.uk> / hgweb
- Shorter proofs and leaner notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Minor updates supplied by the author, mostly connected with a reference to a work by Hilbert, now deleted. — paulson <lp15@cam.ac.uk> / hgweb
- Add a construction, using ZFC_in_HOL, of the category of small sets and functions. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Resolve a "Duplicate constant declaration" issue that occurs with "isabelle build -o export_theory". — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- avoid side effects on working copy while runnign sessions (generated code is unused) — haftmann / hgweb
- clarified formatting, for the sake of scala3; — wenzelm / hgweb
- Deleted a few redundant lines — paulson <lp15@cam.ac.uk> / hgweb
- Trying to beautify this, but it's still ugly — paulson <lp15@cam.ac.uk> / hgweb
- And a bit more tidying — paulson <lp15@cam.ac.uk> / hgweb
- more renaming and tidying — paulson <lp15@cam.ac.uk> / hgweb
- Alphabetic substitutions — paulson <lp15@cam.ac.uk> / hgweb
- Eliminated another finiteness assumption — paulson <lp15@cam.ac.uk> / hgweb
- Removal of some needless finiteness assumptions — paulson <lp15@cam.ac.uk> / hgweb
- Removed a small amount of redundant material from both Szemerédi and Roth — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- tidied up a few proofs — paulson <lp15@cam.ac.uk> / hgweb
- A slightly nicer proof — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- tidied and generalised some proofs using small_eqpoll — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- tidied some proofs — paulson <lp15@cam.ac.uk> / hgweb
- Improved handling splitting theorems in the alphabet command — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Fixed wrong sign handling in fmul-add — Peter Lammich / hgweb
- more count_list lemmas — nipkow / hgweb
- more count_list — nipkow / hgweb
- merged — nipkow / hgweb
- moved some count_list lemmas — nipkow / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- continue 98838b260ed4 — Frédéric Tuong / hgweb
- continue ee01bce2ecca — Frédéric Tuong / hgweb
- cancel some part of 11d4567f1b99 — Frédéric Tuong / hgweb
- cancel some part of 98838b260ed4 — Frédéric Tuong / hgweb
- cancel some part of ada85c62541d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- split locale in two — desharna / hgweb
- Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- added some alternative proofs in Smith_Normal_Form entry — jodivaso / hgweb
- The last tranche of material to be moved to the complex analysis libraries — paulson <lp15@cam.ac.uk> / hgweb
- Removal of material that has since been added to ZFC_in_HOL.General_Cardinals — paulson <lp15@cam.ac.uk> / hgweb
- Deleted nearly 200 lines of unused material — paulson <lp15@cam.ac.uk> / hgweb
- A new theorem — paulson <lp15@cam.ac.uk> / hgweb
- Clarified code module names. — haftmann / hgweb
- removed ancient numeral representation — haftmann / hgweb
- restore state of VYDRA_MDL to b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata for Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- New entry Wetzel's Problem — nipkow / hgweb
- metadata for Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata for VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- Backed out changeset c9f94b0ae10e — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Backed out changeset b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata update for VYDRA_MDL — mraszyk / hgweb
- New entry: VYDRA_MDL — mraszyk / hgweb
- fixed failing proofs — desharna / hgweb
- New definition of the Aleph operator so that it's defined for all arguments, not just ordinals — paulson <lp15@cam.ac.uk> / hgweb
- ALEXANDRIA acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- New set theory lemmas about cardinality (mainly) — paulson <lp15@cam.ac.uk> / hgweb
- Another attempt for a consolidated terminology. — haftmann / hgweb
- Avoid overaggresive splitting. — haftmann / hgweb
- more lemmas for distribution — haftmann / hgweb
- Avoid overaggresive simplification. — haftmann / hgweb
- some new lemmas — paulson <lp15@cam.ac.uk> / hgweb
- merged — nipkow / hgweb
- More material — nipkow / hgweb
- added idempotent most general unifier — desharna / hgweb
- used same parameter order for locales substitution and substitution — desharna / hgweb
- patched for new/simplified lemmas — paulson <lp15@cam.ac.uk> / hgweb
- Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- avoid conflict with index.html in generated html — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry: FO_Theory_Rewriting — nipkow / hgweb
- Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency.
+ Remove obsolete e-mail from notification mailing list. — Emin Karayel <me@eminkarayel.de> / hgweb - Improve proofs for Interpolation_Polynomials_HOL_Algebra.
Reduced the number of apply scripts used. — Emin Karayel <me@eminkarayel.de> / hgweb - Correct date. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- deleted a lemma that's in the devel library — paulson <lp15@cam.ac.uk> / hgweb
- Cleanup and new results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- moved theorems into Matrix.thy — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of AFP 2021-1 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New AFP entry: Equivalence_Relation_Enumeration — nipkow / hgweb
- new entry: LP_Duality — nipkow / hgweb
- cosmetic tweaks — paulson <lp15@cam.ac.uk> / hgweb
- sitegen and metadata for Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Quasi_Borel_Spaces, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Quasi_Borel_Spaces — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
- new entry FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
- tweak: corollary that the ln also yields irrational numbers — paulson <lp15@cam.ac.uk> / hgweb
- New entry: Interpolation_Polynomials_HOL_Algebra — nipkow / hgweb
- Finally remembered to run sitegen — paulson <lp15@cam.ac.uk> / hgweb
- Fixed the meta data in the abstract as well — paulson <lp15@cam.ac.uk> / hgweb
- Eliminated the references to SOS (which is no longer used) and changed to the document style to "article". — paulson <lp15@cam.ac.uk> / hgweb
- typo — nipkow / hgweb
- typo — nipkow / hgweb
- New entry Irrationals_From_THEBOOK — nipkow / hgweb
- new entry Median_Method — nipkow / hgweb
- Actuarial Mathematics website — paulson <lp15@cam.ac.uk> / hgweb
- New entry Actuarial_Mathematics — paulson <lp15@cam.ac.uk> / hgweb
- Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fix LaTeX issue. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Qualification required(?) — nipkow / hgweb
- merged — nipkow / hgweb
- more variants of the algorithm — nipkow / hgweb
- Added funding acknowledgments.
Fixed broken BibTeX citation. — Dominique Unruh <unruh@ut.ee> / hgweb - Strong completeness for PAL systems. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Cleanup. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fewer parentheses around turnstile + remove unused lemmas. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Simplify proof of truth lemma. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Notation for `imply` and fewer parenthesis around turnstiles. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Abstract results to shorten proofs. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merged — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- more symbols; — wenzelm / hgweb
- profer bundle lattice_syntax; — wenzelm / hgweb
- prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended; — wenzelm / hgweb
- Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- avoid hardwired document output; — wenzelm / hgweb
- merged — paulson / hgweb
- deleting the overloading of div and mod, with its attendant ambiguities — paulson <lp15@cam.ac.uk> / hgweb
- replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Removal of a lemma (now in the libraries) and a few tweaks — paulson <lp15@cam.ac.uk> / hgweb
- Tuning. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- merged — paulson / hgweb
- tweaks — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Fixed an inadequate description — paulson <lp15@cam.ac.uk> / hgweb
- tuned — haftmann / hgweb
- mv to distribution — nipkow / hgweb
- by now in distribution — nipkow / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fixed abstract — nipkow / hgweb
- tuned — nipkow / hgweb
- website and metadata for Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sorted ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned — nipkow / hgweb
- New entry Knights_Tour — nipkow / hgweb
- more thoroughly replace Michael Foster's e-mail address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- update Michael Forster's email address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- typo — nipkow / hgweb
- merged — nipkow / hgweb
- New entry Regular_Tree_Relations — nipkow / hgweb
- We DON'T want an output directory — paulson <lp15@cam.ac.uk> / hgweb
- MDP-Algorithms website — paulson <lp15@cam.ac.uk> / hgweb
- new entry MDP-Algorithms — paulson <lp15@cam.ac.uk> / hgweb
- typo — paulson <lp15@cam.ac.uk> / hgweb
- new entry MDP-Rewards — paulson <lp15@cam.ac.uk> / hgweb
- fixed typo — paulson <lp15@cam.ac.uk> / hgweb
- CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- used wfP_imp_asymp from HOL — desharna / hgweb
- simplified proof some more — desharna / hgweb
- simplified proof — desharna / hgweb
- Extended protocol model to support composition of more than two protocols without
the need of re-labeling them, additional automated checks, tighter integration
of the stateful protocol model and the automated verification (PSPSP) tool. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb - Tweaked some failing proofs — paulson <lp15@cam.ac.uk> / hgweb
- adapted to new Sledgehammer.run_sledgehammer return type — desharna / hgweb
- Strengthened a lemma — paulson <lp15@cam.ac.uk> / hgweb
- updated the definition of scheme — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add change history — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- updated 2021-1 release dates -> web — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- ignore generated files — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add 2021-1 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- set devel version again — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added tag Isabelle2021-1 for changeset 11f8b03a88ad — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust usage version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- set release version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
- The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Foundation_of_geometry — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
- adjust for Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Simplicial_complexes_and_boolean_functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust to Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata and sitegen for Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added Mathematics/Measure theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry: Van_Emde_Boas_Trees — nipkow / hgweb
- New entry: Van_Emde_Boas_Trees — nipkow / hgweb
- metadata and sitegen for SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
- A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- generalized standard formula redundancy out of standard redundancy — desharna / hgweb
- merged — wenzelm / hgweb
- discontinued Parse.text; — wenzelm / hgweb
- discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
- weakened locale assumptions: wfP implies asymp — desharna / hgweb
- Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- refactored Standard_Redundancy_Criterion to not use ordering type classes — desharna / hgweb
- isabelle update_cartouches; — wenzelm / hgweb
- removed obsolete "extend" operation; — wenzelm / hgweb
- more symbolic latex_output via XML (using YXML within text);
re-use existing Latex.output_markup; — wenzelm / hgweb - prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust for new tags in Isabelle2021-1-RC4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
- In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
- Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- fixed lemma following Isabelle/c256bba593f3 — desharna / hgweb
#22 (May 2, 2023, 9:49:49 PM)
- test — Fabian Huch <huch@in.tum.de> / hgweb
#21 (Nov 27, 2021, 12:37:17 AM)
- fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
#20 (Nov 26, 2021, 6:59:36 PM)
- fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
#19 (Nov 26, 2021, 3:28:15 PM)
- fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
- A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
- Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself — Dominique Unruh <unruh@ut.ee> / hgweb
- Elimination of all z3 calls — paulson <lp15@cam.ac.uk> / hgweb
- Word_Lib sync from l4v; tweak word_eqI — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- generalise word_eqI method; make sure it is exercised — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- test_bit_size not longer needed; avoid potential nontermination — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Word_Lib tweaks for slightly more backwards compatibility — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- use bit_simps in word_eqI method — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adapted to new version of Infinite_Sum in isabelle-dev — Manuel Eberl <eberlm@in.tum.de> / hgweb
- avoid hardwired document output; — wenzelm / hgweb
- CTR and ETTS: integration with SpecCheck: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
- Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc. — Burkhart Wolff <wolff@lri.fr> / hgweb
- documentation fine-tuning. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Added section on C11_Ast_Lib in chapter II. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Example section restored and Documentation adapted. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Stramge intermediate configuration: Example section zerschossen. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Port to Isabelle2021-1 RC 2. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Improved documentation. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Examples for iterator - applications: queries, and translations into term. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Rearranging standard root store; better documentation in C_Command. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Rearranging the ML _programming Example Section C1. — Burkhart Wolff <wolff@lri.fr> / hgweb
- reorg 1 — Burkhart Wolff <wolff@lri.fr> / hgweb
- ... — Burkhart Wolff <wolff@lri.fr> / hgweb
- Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy) — Burkhart Wolff <wolff@lri.fr> / hgweb
- Restructuring of Interfaces; more show cases. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Updated meta-data for Optics — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Additional scene laws — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Branch merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables. — Simon Foster <simon.foster@york.ac.uk> / hgweb
- feat(SpecCheck/Show) add parentheses for option SOME case — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merged — desharna / hgweb
- weakened ordering requirements — desharna / hgweb
- used well-founded pre-order in standard redundancy criterions — desharna / hgweb
- derived refutational completeness from finitary and non-finitary standard redundancy criterion — desharna / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, since
they are now available as complete methods in Factor-Algebraic-Polynomial — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb - factor_complex_poly delivers distinct list — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merged — paulson / hgweb
- Removal of material that's going to be in Isabelle2021-1 — paulson <lp15@cam.ac.uk> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- refactoring (moving theories and lemmas around) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sync from l4v — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of afp-2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry PAL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Factor_Algebraic_Polynomial — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- document `publish -` — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
- changed affiliation of Eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
- sitegen for Real_Power — paulson <lp15@cam.ac.uk> / hgweb
- new entry Real_Power — paulson <lp15@cam.ac.uk> / hgweb
- New entry Szemeredi_Regularity — nipkow / hgweb
- tuned proofs -- avoid z3; — wenzelm / hgweb
- CTR and ETTS: integration with SpecCheck — user9716869 <user9716869@gmail.com> / hgweb
- used antiquotation to fix LaTeX failure — desharna / hgweb
- adapted to devel — nipkow / hgweb
- updated to devel — nipkow / hgweb
- merged — nipkow / hgweb
- tuned proof for devel — nipkow / hgweb
- clarified quotes vs. apostrophes vs. primes; — wenzelm / hgweb
- more accurate use of LaTeX ndash; — wenzelm / hgweb
- prefer portable LaTeX mdash; — wenzelm / hgweb
- tuned whitespace --- removed suspicious Unicode; — wenzelm / hgweb
- proper Unix linefeeds; — wenzelm / hgweb
- changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
- changed affiliation of eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
- added author to Saturation_Framework_Extensions — desharna / hgweb
- derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy — desharna / hgweb
- added locale calculus_with_finitary_standard_redundancy — desharna / hgweb
- Registers:
- Added mechanism for raising errors if autogenerated files need updating
- Changed definition of Axioms_Quantum.register_pair (returns 0 for incompatible registers, see register_pair_is_register_converse for a useful consequence)
- Slightly reducing namespace pollution in Classical_Extra (hiding consts x, y, X, Y etc.) — Dominique Unruh <unruh@ut.ee> / hgweb - feat(SpecCheck) add better unit tests facilities, examples and exceptions property — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author); — wenzelm / hgweb
- Correctness_Algebras: increase nitpick timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- CZH: dagger monoidal categories — user9716869 <user9716869@gmail.com> / hgweb
- update it Isabelle/925b46043b84 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- sitegen for Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- Correctness_Algebras: increase session timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- tuned signature, according to Isabelle/df12779c3ce8; — wenzelm / hgweb
- feat(SpecCheck) add possibility to make builds fail on failure and extend README — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- added missing funding information — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- restored theory structure for simple genericity. — haftmann / hgweb
- Backed out changeset af549be0a8cd — haftmann / hgweb
- restored different entrance points a before Isabelle2021 — haftmann / hgweb
- proper parentheses (amending 354560d7143a); — wenzelm / hgweb
- Adjusted to prospective release Isabelle2021-2. — haftmann / hgweb
- Correctness_Algebras: uncomment counterexamples — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead; — wenzelm / hgweb
- clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead; — wenzelm / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- remove unused functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- silence sitegen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry X86_Semantics — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust to isabelle@549019b4a808 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata for Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- New entry Correctness_Algebras — nipkow / hgweb
- prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb
- updated metadata for Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- corrected the timeout for CZH_Universal_Constructions — user9716869 <user9716869@gmail.com> / hgweb
- CZH: further results about comma categories and Kan extensions, a variety of other minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- more generic bit/word lemmas for distribution — haftmann / hgweb
- Fixing a name clash between two different "restrict" operators — paulson <lp15@cam.ac.uk> / hgweb
- Merged — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- solved the roots-on-the-border problem — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- split Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- more realistic timeout; — wenzelm / hgweb
- clarified signature, according to Isabelle/ccf599864beb; — wenzelm / hgweb
- back to dedicated separate shift operations for infix syntax;
more default simp rules on closed numeric expressions — haftmann / hgweb
#18 (Oct 22, 2021, 5:09:13 PM)
- modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Various tuning that for some reason didn't get merged from my master branch. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- A spot of polishing — paulson <lp15@cam.ac.uk> / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Update metadata to reflect changes made in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Add a revision note concerning material added in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- tuned signature, according to Isabelle/042041c0ebeb; — wenzelm / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Adjust Imperative List/Map/Set Specification for more lenient next operation
This allows implementations of this iterator specification to make use of
temporary variables for obtaining the next element of the list/set/map.
This is required by some and especially more general iterators. — n.muendler <n.muendler@tum.de> / hgweb - discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
- metadata update for MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
- fixed a mistake in MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted Virtual-Substitution from 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- fixed duplicate "and" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Virtual_Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Virtual Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- updated website/email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
- modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
- modifications in Jinja and DOminance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
- modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
- merged — wenzelm / hgweb
- adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- tuned -- proper names/scopes for contexts; — wenzelm / hgweb
- tuned proofs; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- proper antiquotations; — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
tuned whitespace; — wenzelm / hgweb - dead code!? — wenzelm / hgweb
- clarified signature, following Isabelle/de4f151c2a34; — wenzelm / hgweb
- modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
- CZH: large limits, generalizations, a variety of minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- Simplified a definition — paulson <lp15@cam.ac.uk> / hgweb
- modify propa — nanjiang <nanjiang@whu.edu.cn> / hgweb
- bit singleton shifts recovered for the sake of backward compatibility — haftmann / hgweb
- updated to 7422950f3955 — nipkow / hgweb
- merge — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
- EPO: simplify proof — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
- primer — haftmann / hgweb
- more complete simp rules — haftmann / hgweb
- more complete simp rules (examples) — haftmann / hgweb
- avoid overaggressive contraction of conversions — haftmann / hgweb
- slightly more prominence for proof tools; more examples — haftmann / hgweb
- ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- CTR and ETTS: integration with fd5f62176987 — user9716869 <user9716869@gmail.com> / hgweb
- adapted QHLProver to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
- adapted to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
- adapted to devel — nipkow / hgweb
- Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Weighted_Path_Order: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add missing session dependency — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry FOL_Axiomatic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- minor editorial changes for CZH entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry Weighted_Path_Order — nipkow / hgweb
- fxed metadata (forgot .html) in link — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata and sitegen for complex bounded operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Complex_Bounded_Operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; — wenzelm / hgweb
- clarified timeout;
tuned whitespace; — wenzelm / hgweb - hide_lams ~> opaque_lifting; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- proper inst table; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- proper inst table; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- proper match against const_name; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- fix(ci): clarified addresses, set proper TLS version; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(ci): remove hard-coded address; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(SpecCheck/Show) tune pretty printing for environments — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entries by Mihails Milehins
CZH_Elementary_Categories, CZH_Foundations,
CZH_Universal_Constructions, Conditional_Simplification,
Conditional_Transfer_Rule, Intro_Dest_Elim, and Types_To_Sets_Extension — Gerwin Klein <kleing@unsw.edu.au> / hgweb - New entry: Dominance_CHK — nipkow / hgweb
- Schutz_Spacetime website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Schutz_Spacetime — paulson <lp15@cam.ac.uk> / hgweb
- metadata for Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- repaired slip — haftmann / hgweb
- feat(SpecCheck) folder renaming, types for tests — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- tuned — nipkow / hgweb
- mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f; — wenzelm / hgweb
- ported Design-Theory from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- ported Three-Circles from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- ported Cubic_Quartic_Equations from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Cubic_Quartic_Equations sitegen — paulson <lp15@cam.ac.uk> / hgweb
- new entry Cubic_Quartic_Equations — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for combinatorial design theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Combinatorial Design Theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- clarified modules, according to Isabelle/534b231ce041; — wenzelm / hgweb
- bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax, according to Isabelle/ead56ad40e15;
subtle change of inf (infixl "\<sqinter>" 70) vs. (infixl "\<sqinter>" 65); — wenzelm / hgweb - clarified signature, according to Isabelle/d882abae3379; — wenzelm / hgweb
- explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
- tuned signature, according to Isabelle/28a582aa25dd; — wenzelm / hgweb
- eliminated Specification.definition', following Isabelle/6876e3d5e362; — wenzelm / hgweb
- clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a; — wenzelm / hgweb
- clarified signature, according to Isabelle/612b7e0d6721; — wenzelm / hgweb
- tuned signature, according to Isabelle/839a6e284545; — wenzelm / hgweb
- merged — sterraf / hgweb
- Backed out changeset ef19e4e58b8c
restoring old argument order on synthesized formulas — sterraf / hgweb - avoid hardwired document; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- simplified, using Isabelle/ML operations; — wenzelm / hgweb
- adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- merged — sterraf / hgweb
- synthesized formulas have their variables permuted — sterraf / hgweb
- merged — paulson / hgweb
- fixes for cardinality lemmas — paulson <lp15@cam.ac.uk> / hgweb
- proper inst table; — wenzelm / hgweb
- Graphic rendering of Relational_Method PDF files refined. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
- Entry Relational_Method updated. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
- more realistic timeout; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- follow Isabelle/53e28c438f96; — wenzelm / hgweb
- clarified signature, following Isabelle/a3b0fc510705; — wenzelm / hgweb
- merged — nipkow / hgweb
- tuned — nipkow / hgweb
- consolidation of rules for bit operations — haftmann / hgweb
- tuned name — nipkow / hgweb
- Fix typo — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
- Tune references
... using new name of BD_Security_Compositional — Thomas Bauereiss <thomas@bauereiss.name> / hgweb - Remove redundant license — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
- more realistic timeout: approx. 5min CPU time; — wenzelm / hgweb
- cleaning up — nipkow / hgweb
- New entry CoSMeDis — nipkow / hgweb
- New entry CoSMed — nipkow / hgweb
- New entry: BD_Security_Compositional — nipkow / hgweb
- New entry: CoCon — nipkow / hgweb
- updated to devel — nipkow / hgweb
- merge from AFP 2021 — nipkow / hgweb
- New entry Fresh_Identifiers — nipkow / hgweb
- New entry: Relational_Forests — nipkow / hgweb
- cleaning up — nipkow / hgweb
- merged — nipkow / hgweb
- cleaning up — nipkow / hgweb
- Update Bounded_Deducibility_Security
- Generalise BD Security from I/O automata to nondeterministic transition
systems, with the former retained as an instance of the latter (renaming
locale BD_Security to BD_Security_IO)
- Generalise unwinding conditions to allow making more than one transition at a
time when constructing alternative traces, giving more flexibility for
unwinding strategies
- Add various helper lemmas and definitions
- Add results about the expressivity of declassification triggers vs. bounds,
due to Thomas Bauereiss (added as author) — Thomas Bauereiss <thomas@bauereiss.name> / hgweb - tuned signature, following Isabelle/069f6b2c5a07; — wenzelm / hgweb
- metadata update for MFMC_Countable — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- derive rel_pmf characterization from bounded and unbounded MFMC theorem — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- drop boundedness requirement for the sink — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- avoid global tmp file: pointless due to implicit theory export; — wenzelm / hgweb
- repaired syntax — haftmann / hgweb
- tuned signature, following Isabelle/d030b988d470; — wenzelm / hgweb
- generalized gt_rat_sign_change to square-free polynomials — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- minor updates to bibliography — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- clarified signature; — wenzelm / hgweb
- clarified abstract and concrete boolean algebras — haftmann / hgweb
- antiquotation for bundles — haftmann / hgweb
- simplified hierarchy of type classes for bit operations — haftmann / hgweb
- restored executable conversions — haftmann / hgweb
- dropped junk — haftmann / hgweb
- moved theory Bit_Operations into Main corpus — haftmann / hgweb
- organize syntax for word operations in bundles — haftmann / hgweb
- more systematic approach for instantiation — haftmann / hgweb
- avoid seemingly unused transfer rules — haftmann / hgweb
- cleaner presentation of analysis theorems in preliminaries — yonoteam / hgweb
- Update to new Epistemic_Logic.thy — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Avoid typedefs — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Clean: set AFP standard document options — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Clean: re-add to chapter AFP — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Finitely_Generated_Abelian_Groups website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
- Added Finitely_Generated_Abelian_Groups to metadata — Manuel Eberl <eberlm@in.tum.de> / hgweb
- Sync with my development repo. Add new material: "concrete bicategories" and
"bicategory of categories". Change sublocale declarations related to
functor/natural transformation/natural isomorphism to avoid issues with
global interpretations reported by Filip Smola, 2/2/2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb - compile — blanchet / hgweb
- more realistic timeout: 50min CPU time; — wenzelm / hgweb
- Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending
on Finitely_Generated_Abelian_Groups — Joseph Thommes <joseph-thommes@gmx.de> / hgweb - new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
- remove duplicate entry in metadata — Lars Hupel <lars.hupel@mytum.de> / hgweb
- more coherent dependencies — haftmann / hgweb
- fix(Regex_Equivalence) update to new SpecCheck version — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- operations for symbolic computation of bit operations — haftmann / hgweb
- fixed Proof_Strategy_Language following Isabelle/f58108b7a60c — desharna / hgweb
- SpecCheck now without _ (Regex_Equivalence is still broken) — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- T1 fontenc for new entries — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- update hide_lams -> opaque_lifting — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merged from afp2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- website for SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Public Announcement Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry "Public Announcement Logic"
(and sorted ROOTS + removed duplicate entries in ROOTS) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb - fixed a messy reference — paulson <lp15@cam.ac.uk> / hgweb
- Van_der_Waerden website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Van_der_Waerden — paulson <lp15@cam.ac.uk> / hgweb
- New entry IMP_Compiler — nipkow / hgweb
- Removal of unintended files — Susannah Mansky <susannahej@gmail.com> / hgweb
- Hidden.thy to Isar — Susannah Mansky <susannahej@gmail.com> / hgweb
- merged — desharna / hgweb
- renamed hide_lams opaque_lifting — desharna / hgweb
- merged — Fabian Huch <huch@in.tum.de> / hgweb
- changed to opaque_lifiting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
- changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
#17 (Jul 8, 2021, 12:46:00 PM)
- jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
- Added missing Public_Announcement_Logic to ROOTS file — Manuel Eberl <eberlm@in.tum.de> / hgweb
- More Support on Clean Syntax, Basic Lens Support, New Examples. — Burkhart Wolff <wolff@lri.fr> / hgweb
- finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb
- arg -> Arg: the last holdout — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- arg -> Arg — paulson <lp15@cam.ac.uk> / hgweb
- Add entry public announcement logic — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- adapt to changes in HOL-Library.Cardinality — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- Added Approximation_Algorithm for Center_Selection — nipkow / hgweb
- proved conditional completeness of compilation — desharna / hgweb
- fixed typos — nipkow / hgweb
- more word cleanup — haftmann / hgweb
- more default simp rules — haftmann / hgweb
- some word streamlining — haftmann / hgweb
- made consistent again — haftmann / hgweb
- Fixed entry name for theories in sub-directory — Fabian Huch <huch@in.tum.de> / hgweb