| Author | Object | Transaction | Date |
|---|
| 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 |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP311e9541c68c: added external interface for int/rat-poly factorization, i.e., using integer… | | Tue, Apr 9, 3:53 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFP98b3f6efc0f7: changed definition of square-free-factorization: now [(p1,e1),...,(pn,en)]… | | Tue, Apr 9, 2:28 PM |
| paulson <lp15@cam.ac.uk> | rAFP930a033bce55: The "infinite" typeclass | | Mon, Apr 8, 6:20 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEf7b9179b5029: A bit of new material about type class "infinite", from Eval_FO | | Mon, Apr 8, 5:27 PM |
| paulson <lp15@cam.ac.uk> | rAFPa8e7af355b07: Tidied some ugly proofs | | Mon, Apr 8, 4:44 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPf1f16c6ba99c: added "showl", a class similar to "show", but using String.literal instead… | | Mon, Apr 8, 1:55 PM |
| Rene Thiemann <rene.thiemann@uibk.ac.at> | rAFPaa8210767115: indent, new lemma "inj_show_nat" | | Mon, Apr 8, 1:27 PM |
| paulson <lp15@cam.ac.uk> | rAFP5492883fb017: Uncertainty_Principle sitegen | | Mon, Apr 8, 12:21 PM |
| paulson <lp15@cam.ac.uk> | rAFP4ecda9e9f43b: New entry /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Uncertainty_Princ… | | Mon, Apr 8, 12:15 PM |
| Yosuke-Ito-345 <glacier345@gmail.com> | rAFPc9df2bf00af9: Update | | Sun, Apr 7, 11:18 AM |
| Yosuke-Ito-345 <glacier345@gmail.com> | rAFPa4d44dc12e69: Update | | Sun, Apr 7, 10:35 AM |
| Yosuke-Ito-345 <glacier345@gmail.com> | rAFP2d4043d5d7ce: Update | | Sun, Apr 7, 10:01 AM |
| Yosuke-Ito-345 <glacier345@gmail.com> | rAFPffebb768baf5: Update | | Sun, Apr 7, 8:28 AM |
| Yosuke-Ito-345 <glacier345@gmail.com> | rAFP512d5d0212dc: Update | | Sun, Apr 7, 4:58 AM |
| Yosuke-Ito-345 <glacier345@gmail.com> | rAFP673c1e5b4c02: Update | | Sun, Apr 7, 3:57 AM |
| makarius | rAFP7efa5914d67a: avoid Scala if-expressions and thus make it work both for -new-syntax or -old… | | Apr 5 2024, 10:40 PM |
| makarius | rISABELLE5afbf04418ec: avoid Scala if-expressions and thus make it work both for -new-syntax or -old… | | Apr 5 2024, 9:21 PM |
| makarius | rISABELLEbda75c790bfa: proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); | | Apr 5 2024, 8:41 PM |
| makarius | rISABELLE1b986e5f9764: adjust generated Scala to make it work with scalac -old-syntax and -new-syntax… | | Apr 5 2024, 5:47 PM |
| Simon Wimmer <wimmers@in.tum.de> | rISABELLE5c73934777fc: Add entry on Sketch_and_Explore to CONTRIBUTORS | | Apr 5 2024, 5:10 PM |
| pruvisto | rAFP40bffd87d285: added missing file; simplified proofs | | Apr 5 2024, 3:37 PM |
| pruvisto | rAFP84b1cb16aaf8: simplified proof | | Apr 5 2024, 3:31 PM |
| pruvisto | rAFP1cef82becf2b: tuned abstract for Catalan_Numbers | | Apr 5 2024, 3:22 PM |
| pruvisto | rAFP9e22b9ce09fc: merged | | Apr 5 2024, 10:28 AM |
| pruvisto | rAFP1c6436ee4221: adapted to isabelle/f48f4303c533 | | Apr 4 2024, 10:39 PM |
| makarius | rAFP931936ecb4e1: proper guard to avoid spurious system messages like "### Ignored report message… | | Apr 4 2024, 5:45 PM |
| makarius | rAFPe2ca9e3a5543: tuned: more readable; | | Apr 4 2024, 5:12 PM |
| makarius | rAFP810c04472d86: tuned spelling; | | Apr 4 2024, 4:42 PM |
| makarius | rAFPccce18642d4c: avoid danger of exponental blowup; | | Apr 4 2024, 4:24 PM |
| makarius | rAFP93adc832ec72: avoid aliases of well-known Pure concepts, for the sake of readability; | | Apr 4 2024, 4:21 PM |
| pruvisto | rISABELLE173548e4d5d0: moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL… | | Apr 4 2024, 3:29 PM |
| makarius | rISABELLEe2174bf626b8: more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); | | Apr 4 2024, 11:40 AM |
| makarius | rISABELLE4f9e4527a4e3: tuned signature; | | Apr 4 2024, 11:21 AM |
| pruvisto | rAFPd3cca60aed6b: fixed typos in Hermite_Lindemann | | Apr 4 2024, 10:58 AM |
| desharna | rISABELLE1ca617398213: documented new syntax for fBall and fBex | | Apr 3 2024, 4:55 PM |
| makarius | rWEBSITE37c1362d06cd: update screenshot; | | Apr 3 2024, 3:29 PM |
| makarius | Blog Post: Release Candidates for Isabelle2024 | | Apr 3 2024, 2:57 PM |
| makarius | rWEBSITE4bc2f39188bf: update for release; | | Apr 3 2024, 2:49 PM |
| makarius | rWEBSITEbd4ebadcd3f6: update for release; | | Apr 3 2024, 2:36 PM |
| makarius | rWEBSITE3bede14bad93: merged | | Apr 3 2024, 1:20 PM |
| makarius | rISABELLE1231a7fb2510: misc tuning for release; | | Apr 3 2024, 1:20 PM |
| makarius | rISABELLE01ddd3c203da: Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 | | Apr 3 2024, 1:20 PM |
| makarius | rWEBSITEcff766c2f538: update for release; | | Apr 3 2024, 12:59 PM |
| makarius | rISABELLE6e7f266b9ac2: updated for release; | | Apr 3 2024, 11:35 AM |
| makarius | rAFP12db4a7858c0: proper condition = ISABELLE_GOEXE, to make it work without "isabelle go_setup"; | | Apr 3 2024, 11:31 AM |
| makarius | rISABELLE01ddd3c203da: Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 | | Apr 3 2024, 11:11 AM |
| makarius | rISABELLE1231a7fb2510: misc tuning for release; | | Apr 3 2024, 11:09 AM |
| makarius | rISABELLEee07b7738a24: update for release; | | Apr 3 2024, 11:02 AM |
| makarius | rISABELLEf906f7f83dae: performance tuning: cached non-persistent Parser.gram reduces heap size by… | | Apr 2 2024, 7:32 PM |