| Author | Object | Transaction | Date |
|---|
| 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 |
| 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 |
| 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 |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPb95e62c4c808: provide additional argument so that code-generation in SML/Eval does not fail | | Fri, Apr 12, 12:20 PM |
| paulson | rISABELLE83fa23ca40e5: merged | | Fri, Apr 12, 10:58 AM |
| paulson <lp15@cam.ac.uk> | rISABELLE0f9cd1a5edbe: Tidying ugly proofs | | Fri, Apr 12, 10:58 AM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP8e2e746ba2c0: drop explicit injectivity proof, provide parsers for nat and int instead and… | | Fri, Apr 12, 10:45 AM |
| Fabian Huch <huch@in.tum.de> | rAFPf96cdc08e452: clarified check roots module; | | Fri, Apr 12, 10:27 AM |
| Fabian Huch <huch@in.tum.de> | rAFP05b5fea0d115: tuned; | | Fri, Apr 12, 10:14 AM |
| Fabian Huch <huch@in.tum.de> | rISABELLE5af76462e3a5: tuned; | | Fri, Apr 12, 10:10 AM |
| florian.haftmann | rISABELLE5ed992c47cdc: prefer canonical theorem name for fact collection declarations | | Thu, Apr 11, 8:46 PM |
| Fabian Huch <huch@in.tum.de> | rAFP14d24fbe8ffa: tuned error messages; | | Thu, Apr 11, 3:04 PM |
| pruvisto | rISABELLEc0d689c4fd15: tweaked time functions for median-of-medians selection in HOL-Data_Structures | | Thu, Apr 11, 2:13 PM |
| makarius | rISABELLE2ac132ee8bf1: tuned; | | Thu, Apr 11, 12:12 PM |
| makarius | rISABELLEdbcd6dc7f70f: back to static numa_nodes (reverting part of c2c59de57df9); | | Thu, Apr 11, 12:05 PM |
| makarius | rISABELLE6ec65767d7bd: tuned messages; | | Thu, Apr 11, 12:04 PM |
| Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> | rAFP9bff600ba0bc: updated Standard Borel and S-finite measure monad | | Thu, Apr 11, 11:04 AM |
| Walter Guttmann <walter.guttmann@canterbury.ac.nz> | rAFPa6d153d38d4b: Multirelations_Heterogeneous: added Hoare rules for multirelations | | Thu, Apr 11, 6:17 AM |
| makarius | rAFPc60cdb60c99c: tuned proofs: avoid z3 to make it work on arm64-linux; | | Wed, Apr 10, 11:46 PM |
| makarius | rAFPb5c20c32ec87: tuned proofs: avoid z3 to make it work on arm64-linux; | | Wed, Apr 10, 11:00 PM |
| makarius | rAFPd874320a81ca: tuned proofs: avoid z3 to make it work on arm64-linux; | | Wed, Apr 10, 10:24 PM |
| makarius | rAFP31fcd760227c: tuned proofs: avoid z3 to make it work on arm64-linux; | | Wed, Apr 10, 10:24 PM |
| makarius | rAFPec1c704f4022: tuned proofs: avoid z3 to make it work on arm64-linux; | | Wed, Apr 10, 9:34 PM |
| Asta Halkjær From <andro.from@gmail.com> | rAFP09e32ec351bb: v1.0.1.0 | | Wed, Apr 10, 6:03 PM |
| Asta Halkjær From <andro.from@gmail.com> | rAFPdf6613b912d9: v1.0.1.0 | | Wed, Apr 10, 6:02 PM |
| makarius | rISABELLE1a9f0159de5b: merged | | Wed, Apr 10, 1:23 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE646cd337bb08: Tiny tweaks to proofs | | Wed, Apr 10, 12:32 PM |
| makarius | rISABELLE36389d25d33e: rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04… | | Wed, Apr 10, 11:44 AM |
| Emin Karayel <me@eminkarayel.de> | rAFP1d9d53077605: Median_Method: Add converse of lemma median_est and simplify (corresponding)… | | Wed, Apr 10, 5:34 AM |
| Asta Halkjær From <andro.from@gmail.com> | rAFPe687427e5463: New theory. | | Tue, Apr 9, 7:25 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP05633b57ded4: merge | | Tue, Apr 9, 3:57 PM |