| Author | Object | Transaction | Date |
|---|
| paulson <lp15@cam.ac.uk> | rISABELLEa30a1385f7d0: Starting to tidy HOL-Nominal-Examples | | Sat, Apr 20, 1:08 PM |
| Emin Karayel <me@eminkarayel.de> | rAFPe3e5ef410780: Frequency_Moments: Add tutorial on pseudorandom objects. | | Sat, Apr 20, 7:23 AM |
| Emin Karayel <me@eminkarayel.de> | rAFP716e68f04275: Universal_Hash_Families: Remove obsolete code. | | Sat, Apr 20, 2:47 AM |
| Emin Karayel <me@eminkarayel.de> | rAFP6e02e9bc874d: Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code. | | Sat, Apr 20, 1:58 AM |
| Emin Karayel <me@eminkarayel.de> | rAFP1b546d918c0c: Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various… | | Sat, Apr 20, 1:07 AM |
| paulson | rAFP672eb4689f1a: merged | | Fri, Apr 19, 7:02 PM |
| paulson <lp15@cam.ac.uk> | rAFP8bc05281a185: Exchanged the while-loop and tail-recursive versions of the definitions | | Fri, Apr 19, 7:02 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP3f3f3b9278b9: merge | | Fri, Apr 19, 1:30 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP25dbc1e991c8: rerun sitegen after merge from AFP 2023 | | Fri, Apr 19, 1:26 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP2548b08bc3c4: merge from AFP 2023 | | Fri, Apr 19, 1:11 PM |
| paulson | rAFPac2384b8b86d: merged | | Fri, Apr 19, 1:10 PM |
| paulson <lp15@cam.ac.uk> | rAFP105bd5da5e7e: Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using… | | Fri, Apr 19, 1:10 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP00fb7d6558e5: metadata and sitegen for MFOTL_Checker | | Fri, Apr 19, 1:00 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPcda88c9fcbf9: new entry: MFOTL_Checker | | Fri, Apr 19, 12:24 PM |
| Ata Keskin <ata.keskin@tum.de> | rAFPdb43b58419ea: Removed unnecessary theory file 'Doob_Convergence.thy' | | Fri, Apr 19, 1:49 AM |
| Ata Keskin <ata.keskin@tum.de> | rAFP59321c4a59e5: Updated Doob_Convergence to use the newest version of Martingales | | Fri, Apr 19, 1:42 AM |
| Simon Wimmer <wimmers@in.tum.de> | rISABELLE0c51e0a6bc37: sketch & explore: recover from duplicate fixed variables in Isar proofs | | Thu, Apr 18, 5:53 PM |
| makarius | Blog Post: Release Candidates for Isabelle2024 | | Thu, Apr 18, 4:44 PM |
| makarius | Blog Post: Release Candidates for Isabelle2024 | | Thu, Apr 18, 4:35 PM |
| makarius | Blog Post: Release Candidates for Isabelle2024 | | Thu, Apr 18, 3:53 PM |
| makarius | rISABELLEe07f29df1c67: Added tag Isabelle2024-RC2 for changeset ef2134570abb | | Thu, Apr 18, 3:29 PM |
| makarius | rISABELLEef2134570abb: merged | | Thu, Apr 18, 3:29 PM |
| makarius | rISABELLEbc450c8754ef: merged | | Thu, Apr 18, 3:20 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEe414bcc5a39e: Acknowledgement of Ata Keskin for his Martingales material | | Thu, Apr 18, 2:07 PM |
| makarius | rISABELLE12ce957231e0: back to post-release mode -- after fork point; | | Thu, Apr 18, 1:06 PM |
| makarius | rISABELLEe07f29df1c67: Added tag Isabelle2024-RC2 for changeset ef2134570abb | | Thu, Apr 18, 11:39 AM |
| makarius | rISABELLEef2134570abb: merged | | Wed, Apr 17, 11:22 PM |
| makarius | rISABELLE68fc6839679e: update to jdk-21.0.3; | | Wed, Apr 17, 11:12 PM |
| paulson | rISABELLE8262d4f63b58: merged | | Wed, Apr 17, 11:07 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE601ff5c7cad5: Tidied up horrible archaic proofs | | Wed, Apr 17, 11:07 PM |
| makarius | rISABELLE2fe244c4bb01: clarified signature; | | Wed, Apr 17, 9:20 PM |
| desharna | rAFPd8aa8cc91178: added equivalence of concepts between First_Order_Terms.Position and HOL… | | Wed, Apr 17, 3:58 PM |
| kappelmann | rISABELLE39f9084a9668: make adhoc_overloading respect type constraints | | Wed, Apr 17, 3:04 PM |
| desharna | rAFP900cfb1adad1: added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp] | | Wed, Apr 17, 1:46 PM |
| nipkow | rAFPdbe1aa3fe16e: New entry: ConcurrentHOL | | Wed, Apr 17, 9:52 AM |
| makarius | rISABELLE146468e05dd4: more robust: atomic file-system result via tmp file; | | Tue, Apr 16, 5:53 PM |
| makarius | rISABELLEc729b1d58982: more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4); | | Tue, Apr 16, 5:53 PM |
| makarius | rISABELLEab07d4cb7d1c: removed junk (amending 8cd399b25dac); | | Tue, Apr 16, 5:53 PM |
| makarius | rISABELLEc2c59de57df9: clarified static Build_Process.Context vs. dynamic Build_Process.State; | | Tue, Apr 16, 5:53 PM |
| makarius | rISABELLEdbcd6dc7f70f: back to static numa_nodes (reverting part of c2c59de57df9); | | Tue, Apr 16, 5:53 PM |
| makarius | rISABELLEb73df63e0f52: merged | | Tue, Apr 16, 5:28 PM |
| makarius | rISABELLE761bd2b35217: tuned; | | Tue, Apr 16, 5:06 PM |
| makarius | rISABELLE455ddb251ece: clarified signature; | | Tue, Apr 16, 4:54 PM |
| makarius | rISABELLE05cec0a3c63d: clarified modules and options (from store); | | Tue, Apr 16, 4:53 PM |
| makarius | rISABELLE7e4c3bb3d062: minor performance tuning: avoid redundant server access; | | Tue, Apr 16, 4:38 PM |
| makarius | rISABELLE66d7a923b750: tuned; | | Tue, Apr 16, 4:37 PM |
| makarius | rISABELLE370ebda8bd86: clarified signature; | | Tue, Apr 16, 4:27 PM |
| makarius | rISABELLE47f671888a37: tuned; | | Tue, Apr 16, 3:14 PM |
| makarius | rISABELLE0323cd9fcab9: clarified signature; | | Tue, Apr 16, 3:11 PM |
| makarius | rISABELLE61b8f6ac6860: tuned signature; | | Tue, Apr 16, 2:48 PM |
| pruvisto | rISABELLE247751d25102: canonical time function for List.nth | | Tue, Apr 16, 1:29 PM |
| makarius | rISABELLEd510a1cf9965: tuned; | | Tue, Apr 16, 12:18 PM |
| makarius | rISABELLEd4d9a7887b2a: tuned signature; | | Tue, Apr 16, 12:08 PM |
| makarius | rISABELLEc188068e41f1: tuned; | | Tue, Apr 16, 11:39 AM |
| makarius | rISABELLE4b95a1d8b2c9: tuned; | | Tue, Apr 16, 11:20 AM |
| makarius | rISABELLEc729b1d58982: more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4); | | Tue, Apr 16, 11:00 AM |
| paulson | rISABELLE693d4e6cc5b8: merged | | Mon, Apr 15, 11:24 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE2fa018321400: Streamlining of many more archaic proofs | | Mon, Apr 15, 11:23 PM |
| Fabian Huch <huch@in.tum.de> | rISABELLE138b5172c7f8: clarified web app parameters: more flexible, using HTML5 id specification… | | Mon, Apr 15, 8:35 PM |
| Fabian Huch <huch@in.tum.de> | rAFP7f16aa37c534: proper getopts; | | Mon, Apr 15, 8:11 PM |
| Fabian Huch <huch@in.tum.de> | rAFP5b2e7d535aff: tuned: use explicit keys; | | Mon, Apr 15, 7:36 PM |
| nipkow | rAFP114c5bc73eff: merged | | Mon, Apr 15, 6:05 PM |
| nipkow | rAFP95692a54af6b: tuned names | | Mon, Apr 15, 6:04 PM |
| Fabian Huch <huch@in.tum.de> | rAFP2f55893686bc: tuned; | | Mon, Apr 15, 5:50 PM |
| Thibault Dardinier <thibault.dardinier@inf.ethz.ch> | rAFP408a29902df3: Removed inactive DOI | | Mon, Apr 15, 5:48 PM |
| Thibault Dardinier <thibault.dardinier@inf.ethz.ch> | rAFPe0dfdf1b8ed4: Removed inactive DOI | | Mon, Apr 15, 5:48 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPd81723aa95cb: added monotonicity lemmas of lex/mul-ext | | Mon, Apr 15, 4:53 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPd8fb49658d5f: more showl-real instantiation to Show_Real thy | | Mon, Apr 15, 4:10 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP1c2509fdeac7: added showl-functions for terms and contexts | | Mon, Apr 15, 3:55 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPa52546d735ec: merge | | Mon, Apr 15, 1:55 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPc61a0a701a26: added many results on first-order terms, added positions | | Mon, Apr 15, 1:54 PM |
| Fabian Huch <huch@in.tum.de> | rAFPeaea08280462: updated docs; | | Mon, Apr 15, 1:31 PM |
| Fabian Huch <huch@in.tum.de> | rAFPc34ca8a848b0: proper keys (amending 36cf00eeb9e4); | | Mon, Apr 15, 1:17 PM |
| Fabian Huch <huch@in.tum.de> | rAFP36cf00eeb9e4: moved web_app to distribution (see Isabelle/37ea0727291f); | | Mon, Apr 15, 1:17 PM |
| Fabian Huch <huch@in.tum.de> | rAFPc34ca8a848b0: proper keys (amending 36cf00eeb9e4); | | Mon, Apr 15, 1:16 PM |
| Fabian Huch <huch@in.tum.de> | rAFP6539b6f3e1cf: add separate Isabelle tool for metadata editing; | | Mon, Apr 15, 1:04 PM |
| Fabian Huch <huch@in.tum.de> | rAFPd2e29e073f08: better defaults; | | Mon, Apr 15, 11:21 AM |
| Fabian Huch <huch@in.tum.de> | rAFPbec250baad75: clarified AFP base dir: usually given by environment; | | Mon, Apr 15, 11:08 AM |
| Fabian Huch <huch@in.tum.de> | rAFP8fd1acd065c6: activate slow metadata checks by default; | | Mon, Apr 15, 10:47 AM |
| Fabian Huch <huch@in.tum.de> | rAFP20b8a26117af: Updated HyperHoareLogic entry: Additional rules | | Mon, Apr 15, 10:04 AM |
| Fabian Huch <huch@in.tum.de> | rAFPbd75044b84f8: fix broken metadata introduced by 20b8a26117af; | | Mon, Apr 15, 10:04 AM |
| Fabian Huch <huch@in.tum.de> | rAFPbd75044b84f8: fix broken metadata introduced by 20b8a26117af; | | Mon, Apr 15, 10:00 AM |
| paulson <lp15@cam.ac.uk> | rISABELLE577a2896ace9: More tidying of old proofs | | Sun, Apr 14, 11:38 PM |
| paulson | rISABELLEfddf8d9c8083: merged | | Sun, Apr 14, 7:39 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE2ff4cc7fa70a: More tidying and removal of "apply" | | Sun, Apr 14, 7:39 PM |
| makarius | Blog Post: Release Candidates for Isabelle2024 | | Sun, Apr 14, 1:24 PM |
| Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> | rAFP81de808826f9: updated:Standard_Borel_Spaces | | Sun, Apr 14, 7:58 AM |
| Simon Wimmer <wimmers@in.tum.de> | rISABELLE7506cb70ecfb: Add subgoals variant of 'sketch' command | | Sat, Apr 13, 10:22 AM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP2db006965e8e: fix document generator: _ -> - | | Sat, Apr 13, 8:02 AM |
| Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> | rAFP62f87ac53318: update: Standard_Borel_Spaces | | Sat, Apr 13, 1:34 AM |
| paulson | rISABELLEc111785fd640: merged | | Fri, Apr 12, 11:19 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEc06c95576ea9: Tidied some messy proofs | | Fri, Apr 12, 11:19 PM |
| makarius | rISABELLEf4d3e3915228: tuned messages; | | Fri, Apr 12, 5:07 PM |
| Thibault Dardinier <thibault.dardinier@inf.ethz.ch> | rAFPbbd1dc798620: Merged | | Fri, Apr 12, 3:45 PM |
| Thibault Dardinier <thibault.dardinier@inf.ethz.ch> | rAFP20b8a26117af: Updated HyperHoareLogic entry: Additional rules | | Fri, Apr 12, 3:45 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPf7ec8c203092: tune imports | | Fri, Apr 12, 2:49 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPc60abfef602f: polished theory | | Fri, Apr 12, 2:35 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPf5b7116751a9: documented recent changes | | Fri, Apr 12, 12:30 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP43c62567dc63: documented changes in Show-entry | | Fri, Apr 12, 12:28 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPb086e875e09b: use new XML-transformer from IsaFoR, developed by A. Yamada | | Fri, Apr 12, 12:25 PM |