| Author | Object | Transaction | Date |
|---|
| 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… | | Fri, Apr 5, 10:40 PM |
| makarius | rISABELLE5afbf04418ec: avoid Scala if-expressions and thus make it work both for -new-syntax or -old… | | Fri, Apr 5, 9:21 PM |
| makarius | rISABELLEbda75c790bfa: proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); | | Fri, Apr 5, 8:41 PM |
| makarius | rISABELLE1b986e5f9764: adjust generated Scala to make it work with scalac -old-syntax and -new-syntax… | | Fri, Apr 5, 5:47 PM |
| Simon Wimmer <wimmers@in.tum.de> | rISABELLE5c73934777fc: Add entry on Sketch_and_Explore to CONTRIBUTORS | | Fri, Apr 5, 5:10 PM |
| pruvisto | rAFP40bffd87d285: added missing file; simplified proofs | | Fri, Apr 5, 3:37 PM |
| pruvisto | rAFP84b1cb16aaf8: simplified proof | | Fri, Apr 5, 3:31 PM |
| pruvisto | rAFP1cef82becf2b: tuned abstract for Catalan_Numbers | | Fri, Apr 5, 3:22 PM |
| pruvisto | rAFP9e22b9ce09fc: merged | | Fri, Apr 5, 10:28 AM |
| pruvisto | rAFP1c6436ee4221: adapted to isabelle/f48f4303c533 | | Thu, Apr 4, 10:39 PM |
| makarius | rAFP931936ecb4e1: proper guard to avoid spurious system messages like "### Ignored report message… | | Thu, Apr 4, 5:45 PM |
| makarius | rAFPe2ca9e3a5543: tuned: more readable; | | Thu, Apr 4, 5:12 PM |
| makarius | rAFP810c04472d86: tuned spelling; | | Thu, Apr 4, 4:42 PM |
| makarius | rAFPccce18642d4c: avoid danger of exponental blowup; | | Thu, Apr 4, 4:24 PM |
| makarius | rAFP93adc832ec72: avoid aliases of well-known Pure concepts, for the sake of readability; | | Thu, Apr 4, 4:21 PM |
| pruvisto | rISABELLE173548e4d5d0: moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL… | | Thu, Apr 4, 3:29 PM |
| makarius | rISABELLEe2174bf626b8: more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); | | Thu, Apr 4, 11:40 AM |
| makarius | rISABELLE4f9e4527a4e3: tuned signature; | | Thu, Apr 4, 11:21 AM |
| pruvisto | rAFPd3cca60aed6b: fixed typos in Hermite_Lindemann | | Thu, Apr 4, 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 |
| makarius | rISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to… | | Apr 2 2024, 7:32 PM |
| makarius | rISABELLEd67cacd09251: merged | | Apr 2 2024, 7:18 PM |
| Lars Hupel <lars@hupel.info> | rAFP0d5e63bc2b19: merged | | Apr 2 2024, 7:11 PM |
| makarius | rISABELLE09e9819beef6: update to stack-2.15.5, stackage-lts-22.15; | | Apr 2 2024, 7:10 PM |
| makarius | rISABELLE951c371c1cd9: clarified names: discontinue odd convention from 3 decades ago; | | Apr 2 2024, 6:29 PM |
| pruvisto | rISABELLE33a9b1d6a651: added documentation for meromorphicity etc. in HOL-Complex_Analysis | | Apr 2 2024, 6:02 PM |
| makarius | rISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to… | | Apr 2 2024, 5:20 PM |
| desharna | rAFP424dc98e93ad: adapted to Isabelle/67e77f1e6d7b | | Apr 2 2024, 4:34 PM |
| desharna | rISABELLE67e77f1e6d7b: added special syntax for FSet.Ball and FSet.Bex | | Apr 2 2024, 4:34 PM |
| desharna | rISABELLE876bb57e7376: merged | | Apr 2 2024, 4:33 PM |
| desharna | rAFP424dc98e93ad: adapted to Isabelle/67e77f1e6d7b | | Apr 2 2024, 4:33 PM |
| makarius | rAFP5819f2a448d6: tuned proofs: avoid z3 to make it work on arm64-linux; | | Apr 2 2024, 2:53 PM |
| traytel | rAFP51fb7da70175: sitegen for Broadcast_Psi | | Apr 2 2024, 2:34 PM |
| traytel | rAFP31ea85757858: new entry Broadcast_Psi | | Apr 2 2024, 1:29 PM |
| Lars Hupel <lars@hupel.info> | rAFPa8ac72f7dd9f: make Go test mandatory | | Apr 2 2024, 11:51 AM |
| Lars Hupel <lars@hupel.info> | rAFP985b115c06a9: remove generated files | | Apr 2 2024, 11:42 AM |
| Lars Hupel <lars@hupel.info> | rISABELLEd6a787ccf583: remove transitional (dummy) component list for Go | | Apr 2 2024, 11:26 AM |
| Lars Hupel <lars@hupel.info> | rAFP33a266b1265e: remove "horrible workaround", fixed in upstream Isabelle (authored by Terru) | | Apr 2 2024, 9:47 AM |
| desharna | rISABELLE6de94d690f9f: merged | | Apr 2 2024, 8:35 AM |
| makarius | rAFPc99fa2f32389: tuned proofs: avoid z3 to make it work on arm64-linux; | | Apr 1 2024, 10:33 PM |
| makarius | rAFP4034bbbba794: tuned proofs: avoid z3 to make it work on arm64-linux; | | Apr 1 2024, 9:34 PM |
| makarius | rAFPde38656982c3: tuned whitespace; | | Apr 1 2024, 7:13 PM |
| makarius | rISABELLE9c00a46d69d0: new simplifier trace_op for tracing simproc calls | | Apr 1 2024, 7:06 PM |