- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Today
Today
Emin Karayel <me@eminkarayel.de> committed rAFPe3e5ef410780: Frequency_Moments: Add tutorial on pseudorandom objects..
Frequency_Moments: Add tutorial on pseudorandom objects.
Emin Karayel <me@eminkarayel.de> committed rAFP716e68f04275: Universal_Hash_Families: Remove obsolete code..
Universal_Hash_Families: Remove obsolete code.
Emin Karayel <me@eminkarayel.de> committed rAFP6e02e9bc874d: Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code..
Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code.
Emin Karayel <me@eminkarayel.de> committed rAFP1b546d918c0c: Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various….
Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various…
Yesterday
Yesterday
paulson <lp15@cam.ac.uk> committed rAFP8bc05281a185: Exchanged the while-loop and tail-recursive versions of the definitions.
Exchanged the while-loop and tail-recursive versions of the definitions
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2548b08bc3c4: merge from AFP 2023.
merge from AFP 2023
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP3f3f3b9278b9: merge.
merge
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP00fb7d6558e5: metadata and sitegen for MFOTL_Checker.
metadata and sitegen for MFOTL_Checker
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP25dbc1e991c8: rerun sitegen after merge from AFP 2023.
rerun sitegen after merge from AFP 2023
nipkow committed rAFPdbe1aa3fe16e: New entry: ConcurrentHOL.
New entry: ConcurrentHOL
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPcda88c9fcbf9: new entry: MFOTL_Checker.
new entry: MFOTL_Checker
paulson <lp15@cam.ac.uk> committed rAFP5492883fb017: Uncertainty_Principle sitegen.
Uncertainty_Principle sitegen
paulson <lp15@cam.ac.uk> committed rAFP4ecda9e9f43b: New entry /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Uncertainty_Princ….
New entry /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Uncertainty_Princ…
sitegen for Broadcast_Psi
new entry Broadcast_Psi
paulson <lp15@cam.ac.uk> committed rAFP105bd5da5e7e: Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using….
Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using…
Ata Keskin <ata.keskin@tum.de> committed rAFPdb43b58419ea: Removed unnecessary theory file 'Doob_Convergence.thy'.
Removed unnecessary theory file 'Doob_Convergence.thy'
Ata Keskin <ata.keskin@tum.de> committed rAFP59321c4a59e5: Updated Doob_Convergence to use the newest version of Martingales.
Updated Doob_Convergence to use the newest version of Martingales
Thu, Apr 18
Thu, Apr 18
Simon Wimmer <wimmers@in.tum.de> committed rISABELLE0c51e0a6bc37: sketch & explore: recover from duplicate fixed variables in Isar proofs.
sketch & explore: recover from duplicate fixed variables in Isar proofs
back to post-release mode -- after fork point;
Added tag Isabelle2024-RC2 for changeset ef2134570abb
paulson <lp15@cam.ac.uk> committed rISABELLEe414bcc5a39e: Acknowledgement of Ata Keskin for his Martingales material.
Acknowledgement of Ata Keskin for his Martingales material
desharna committed rAFPd8aa8cc91178: added equivalence of concepts between First_Order_Terms.Position and HOL….
added equivalence of concepts between First_Order_Terms.Position and HOL…
Wed, Apr 17
Wed, Apr 17
update to jdk-21.0.3;
paulson <lp15@cam.ac.uk> committed rISABELLE601ff5c7cad5: Tidied up horrible archaic proofs.
Tidied up horrible archaic proofs
clarified signature;
make adhoc_overloading respect type constraints
desharna committed rAFP900cfb1adad1: added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp].
added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp]
Tue, Apr 16
Tue, Apr 16
clarified signature;
minor performance tuning: avoid redundant server access;
clarified modules and options (from store);
clarified signature;
clarified signature;
makarius committed rISABELLEc729b1d58982: more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);.
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
makarius committed rISABELLEdbcd6dc7f70f: back to static numa_nodes (reverting part of c2c59de57df9);.
back to static numa_nodes (reverting part of c2c59de57df9);
canonical time function for List.nth
Mon, Apr 15
Mon, Apr 15
paulson <lp15@cam.ac.uk> committed rISABELLE2fa018321400: Streamlining of many more archaic proofs.
Streamlining of many more archaic proofs
Fabian Huch <huch@in.tum.de> committed rISABELLE138b5172c7f8: clarified web app parameters: more flexible, using HTML5 id specification….
clarified web app parameters: more flexible, using HTML5 id specification…
Fabian Huch <huch@in.tum.de> committed rAFP7f16aa37c534: proper getopts;.
proper getopts;
Fabian Huch <huch@in.tum.de> committed rAFP5b2e7d535aff: tuned: use explicit keys;.
tuned: use explicit keys;
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFP408a29902df3: Removed inactive DOI.
Removed inactive DOI
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFPe0dfdf1b8ed4: Removed inactive DOI.
Removed inactive DOI
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd81723aa95cb: added monotonicity lemmas of lex/mul-ext.
added monotonicity lemmas of lex/mul-ext
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd8fb49658d5f: more showl-real instantiation to Show_Real thy.
more showl-real instantiation to Show_Real thy
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1c2509fdeac7: added showl-functions for terms and contexts.
added showl-functions for terms and contexts
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPc61a0a701a26: added many results on first-order terms, added positions.
added many results on first-order terms, added positions
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa52546d735ec: merge.
merge
Fabian Huch <huch@in.tum.de> committed rAFPeaea08280462: updated docs;.
updated docs;
Fabian Huch <huch@in.tum.de> committed rAFPc34ca8a848b0: proper keys (amending 36cf00eeb9e4);.
proper keys (amending 36cf00eeb9e4);
Fabian Huch <huch@in.tum.de> committed rAFP6539b6f3e1cf: add separate Isabelle tool for metadata editing;.
add separate Isabelle tool for metadata editing;
Fabian Huch <huch@in.tum.de> committed rAFPd2e29e073f08: better defaults;.
better defaults;
Fabian Huch <huch@in.tum.de> committed rAFPbec250baad75: clarified AFP base dir: usually given by environment;.
clarified AFP base dir: usually given by environment;
Fabian Huch <huch@in.tum.de> committed rAFP8fd1acd065c6: activate slow metadata checks by default;.
activate slow metadata checks by default;
Fabian Huch <huch@in.tum.de> committed rAFPbd75044b84f8: fix broken metadata introduced by 20b8a26117af;.
fix broken metadata introduced by 20b8a26117af;
Sun, Apr 14
Sun, Apr 14
paulson <lp15@cam.ac.uk> committed rISABELLE577a2896ace9: More tidying of old proofs.
More tidying of old proofs
paulson <lp15@cam.ac.uk> committed rISABELLE2ff4cc7fa70a: More tidying and removal of "apply".
More tidying and removal of "apply"
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFP81de808826f9: updated:Standard_Borel_Spaces.
updated:Standard_Borel_Spaces
Sat, Apr 13
Sat, Apr 13
Simon Wimmer <wimmers@in.tum.de> committed rISABELLE7506cb70ecfb: Add subgoals variant of 'sketch' command.
Add subgoals variant of 'sketch' command
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2db006965e8e: fix document generator: _ -> -.
fix document generator: _ -> -
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFP62f87ac53318: update: Standard_Borel_Spaces.
update: Standard_Borel_Spaces
Fri, Apr 12
Fri, Apr 12
paulson <lp15@cam.ac.uk> committed rISABELLEc06c95576ea9: Tidied some messy proofs.
Tidied some messy proofs
florian.haftmann committed rISABELLE5ed992c47cdc: prefer canonical theorem name for fact collection declarations.
prefer canonical theorem name for fact collection declarations
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFPbbd1dc798620: Merged.
Merged
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFP20b8a26117af: Updated HyperHoareLogic entry: Additional rules.
Updated HyperHoareLogic entry: Additional rules
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf7ec8c203092: tune imports.
tune imports
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPc60abfef602f: polished theory.
polished theory
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf5b7116751a9: documented recent changes.
documented recent changes
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP43c62567dc63: documented changes in Show-entry.
documented changes in Show-entry
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb95e62c4c808: provide additional argument so that code-generation in SML/Eval does not fail.
provide additional argument so that code-generation in SML/Eval does not fail
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb086e875e09b: use new XML-transformer from IsaFoR, developed by A. Yamada.
use new XML-transformer from IsaFoR, developed by A. Yamada
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP8e2e746ba2c0: drop explicit injectivity proof, provide parsers for nat and int instead and….
drop explicit injectivity proof, provide parsers for nat and int instead and…
paulson <lp15@cam.ac.uk> committed rISABELLE0f9cd1a5edbe: Tidying ugly proofs.
Tidying ugly proofs