Author | Object | Transaction | Date |
---|
makarius | rISABELLE96f60533ec1d: update Windows test machines; | | Fri, Apr 26, 1:25 PM |
makarius | Blog Post: Release Candidates for Isabelle2024 | | Thu, Apr 25, 5:01 PM |
paulson <lp15@cam.ac.uk> | rISABELLE40a3fc07a587: More tidying of proofs | | Wed, Apr 24, 9:56 PM |
makarius | rAFPecd8c892f11e: tuned proofs: make it work on Windows; | | Wed, Apr 24, 2:15 PM |
makarius | rAFPf79070b39fe2: proper platform_path for Windows; | | Wed, Apr 24, 2:05 PM |
makarius | rAFP29314eac2682: more robust and more portable, notably for Windows; | | Wed, Apr 24, 1:36 PM |
paulson <lp15@cam.ac.uk> | rISABELLEb156869b826a: Another Nominal example | | Wed, Apr 24, 10:21 AM |
paulson | rISABELLE8e168a3d2a23: merged | | Tue, Apr 23, 10:58 PM |
paulson <lp15@cam.ac.uk> | rISABELLEcf11a7f0a5f0: Tidying up another Nominal example (SOS) | | Tue, Apr 23, 10:58 PM |
Achim D. Brucker <adbrucker@0x5f.org> | rAFP0e05592c7e5e: Removed obsolete LaTeX commands. | | Tue, Apr 23, 10:44 PM |
makarius | rISABELLE0eff7d113549: update Windows build host; | | Tue, Apr 23, 3:57 PM |
makarius | rISABELLEcfe18c31725c: proper command-line; | | Tue, Apr 23, 3:56 PM |
paulson <lp15@cam.ac.uk> | rISABELLE378593bf5109: Tidying up another of the nominal examples | | Tue, Apr 23, 11:26 AM |
paulson <lp15@cam.ac.uk> | rISABELLE34e0ddfc6dcc: More tidying of Nominal proofs | | Mon, Apr 22, 11:08 PM |
nipkow | rAFPa23e9762512e: added contributor | | Mon, Apr 22, 3:01 PM |
paulson <lp15@cam.ac.uk> | rISABELLE022a9c26b14f: Tidied up another messy theory | | Mon, Apr 22, 11:43 AM |
paulson <lp15@cam.ac.uk> | rISABELLE6d56e85f674e: More proof tidying for Nominal | | Sun, Apr 21, 5:31 PM |
kappelmann | rAFP3133b6848037: merged | | Sun, Apr 21, 12:35 PM |
kappelmann | rAFP2a6196e5b347: feat(Transport) add simpler function type introduction rule for extend | | Sun, Apr 21, 12:33 PM |
kappelmann | rAFP237996782d80: feat(Transport) functions as binary relations, improved mono notation, make non… | | Sun, Apr 21, 12:12 PM |
kappelmann | rAFPfe57a84f565f: feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems… | | Sun, Apr 21, 10:06 AM |
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> | rAFPf3289a39d4bf: updated:Standard Borel Spaces | | Sun, Apr 21, 2:25 AM |
paulson <lp15@cam.ac.uk> | rISABELLEfec5a23017b5: Tidying up more messy proofs | | Sun, Apr 21, 12:02 AM |
Dominique Unruh <hg.yse9he@rwth.unruh.de> | rAFP22721115789f: Miscellaneous changes to Complex_Bounded_Operators. | | Sat, Apr 20, 11:29 PM |
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 |