| Author | Object | Transaction | Date |
|---|
| 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 | | Wed, Apr 3, 4:55 PM |
| makarius | rWEBSITE37c1362d06cd: update screenshot; | | Wed, Apr 3, 3:29 PM |
| makarius | Blog Post: Release Candidates for Isabelle2024 | | Wed, Apr 3, 2:57 PM |
| makarius | rWEBSITE4bc2f39188bf: update for release; | | Wed, Apr 3, 2:49 PM |
| makarius | rWEBSITEbd4ebadcd3f6: update for release; | | Wed, Apr 3, 2:36 PM |
| makarius | rWEBSITE3bede14bad93: merged | | Wed, Apr 3, 1:20 PM |
| makarius | rISABELLE1231a7fb2510: misc tuning for release; | | Wed, Apr 3, 1:20 PM |
| makarius | rISABELLE01ddd3c203da: Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 | | Wed, Apr 3, 1:20 PM |
| makarius | rWEBSITEcff766c2f538: update for release; | | Wed, Apr 3, 12:59 PM |
| makarius | rISABELLE6e7f266b9ac2: updated for release; | | Wed, Apr 3, 11:35 AM |
| makarius | rAFP12db4a7858c0: proper condition = ISABELLE_GOEXE, to make it work without "isabelle go_setup"; | | Wed, Apr 3, 11:31 AM |
| makarius | rISABELLE01ddd3c203da: Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 | | Wed, Apr 3, 11:11 AM |
| makarius | rISABELLE1231a7fb2510: misc tuning for release; | | Wed, Apr 3, 11:09 AM |
| makarius | rISABELLEee07b7738a24: update for release; | | Wed, Apr 3, 11:02 AM |
| makarius | rISABELLEf906f7f83dae: performance tuning: cached non-persistent Parser.gram reduces heap size by… | | Tue, Apr 2, 7:32 PM |
| makarius | rISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to… | | Tue, Apr 2, 7:32 PM |
| makarius | rISABELLEd67cacd09251: merged | | Tue, Apr 2, 7:18 PM |
| Lars Hupel <lars@hupel.info> | rAFP0d5e63bc2b19: merged | | Tue, Apr 2, 7:11 PM |
| makarius | rISABELLE09e9819beef6: update to stack-2.15.5, stackage-lts-22.15; | | Tue, Apr 2, 7:10 PM |
| makarius | rISABELLE951c371c1cd9: clarified names: discontinue odd convention from 3 decades ago; | | Tue, Apr 2, 6:29 PM |
| pruvisto | rISABELLE33a9b1d6a651: added documentation for meromorphicity etc. in HOL-Complex_Analysis | | Tue, Apr 2, 6:02 PM |
| makarius | rISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to… | | Tue, Apr 2, 5:20 PM |
| desharna | rAFP424dc98e93ad: adapted to Isabelle/67e77f1e6d7b | | Tue, Apr 2, 4:34 PM |
| desharna | rISABELLE67e77f1e6d7b: added special syntax for FSet.Ball and FSet.Bex | | Tue, Apr 2, 4:34 PM |
| desharna | rISABELLE876bb57e7376: merged | | Tue, Apr 2, 4:33 PM |
| desharna | rAFP424dc98e93ad: adapted to Isabelle/67e77f1e6d7b | | Tue, Apr 2, 4:33 PM |
| makarius | rAFP5819f2a448d6: tuned proofs: avoid z3 to make it work on arm64-linux; | | Tue, Apr 2, 2:53 PM |
| traytel | rAFP51fb7da70175: sitegen for Broadcast_Psi | | Tue, Apr 2, 2:34 PM |
| traytel | rAFP31ea85757858: new entry Broadcast_Psi | | Tue, Apr 2, 1:29 PM |
| Lars Hupel <lars@hupel.info> | rAFPa8ac72f7dd9f: make Go test mandatory | | Tue, Apr 2, 11:51 AM |
| Lars Hupel <lars@hupel.info> | rAFP985b115c06a9: remove generated files | | Tue, Apr 2, 11:42 AM |
| Lars Hupel <lars@hupel.info> | rISABELLEd6a787ccf583: remove transitional (dummy) component list for Go | | Tue, Apr 2, 11:26 AM |
| Lars Hupel <lars@hupel.info> | rAFP33a266b1265e: remove "horrible workaround", fixed in upstream Isabelle (authored by Terru) | | Tue, Apr 2, 9:47 AM |
| desharna | rISABELLE6de94d690f9f: merged | | Tue, Apr 2, 8:35 AM |
| makarius | rAFPc99fa2f32389: tuned proofs: avoid z3 to make it work on arm64-linux; | | Mon, Apr 1, 10:33 PM |
| makarius | rAFP4034bbbba794: tuned proofs: avoid z3 to make it work on arm64-linux; | | Mon, Apr 1, 9:34 PM |
| makarius | rAFPde38656982c3: tuned whitespace; | | Mon, Apr 1, 7:13 PM |
| makarius | rISABELLE9c00a46d69d0: new simplifier trace_op for tracing simproc calls | | Mon, Apr 1, 7:06 PM |
| makarius | rISABELLEc5cd7a58cf2d: generic trace operations for main steps of Simplifier; | | Mon, Apr 1, 7:06 PM |
| makarius | rISABELLE0d94dd2fd2d0: clarified names (see also 9c00a46d69d0, c5cd7a58cf2d); | | Mon, Apr 1, 7:06 PM |
| makarius | rISABELLE06153e2e0cdb: more official AFP.groups; | | Mon, Apr 1, 7:06 PM |
| makarius | rISABELLE1478c6d52864: clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that… | | Mon, Apr 1, 7:06 PM |
| makarius | rAFP0c06ebfbaba1: tuned proofs: avoid z3 to make it work on arm64-linux; | | Mon, Apr 1, 6:46 PM |
| makarius | rAFPc1af731e14b9: tuned proofs: avoid z3 to make it work on arm64-linux; | | Mon, Apr 1, 6:46 PM |
| makarius | rISABELLE60b6c735b5d5: clarified signature: prefer authentic cterm used in Simplifier, avoid potential… | | Mon, Apr 1, 3:47 PM |
| makarius | rISABELLE0d94dd2fd2d0: clarified names (see also 9c00a46d69d0, c5cd7a58cf2d); | | Mon, Apr 1, 3:37 PM |
| makarius | rISABELLE588ea80f16bb: provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version; | | Mon, Apr 1, 3:09 PM |
| makarius | rISABELLE1478c6d52864: clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that… | | Mon, Apr 1, 2:36 PM |
| pruvisto | rAFP1cd8d5cb1636: adapted Zeta_3_Irrational w.r.t. isabelle/4c1347e172b1 | | Mar 30 2024, 9:18 PM |
| pruvisto | rISABELLE4c1347e172b1: moved over material from AFP; most importantly on algebraic numbers and… | | Mar 30 2024, 9:18 PM |
| pruvisto | rAFP1cd8d5cb1636: adapted Zeta_3_Irrational w.r.t. isabelle/4c1347e172b1 | | Mar 30 2024, 9:17 PM |
| pruvisto | rISABELLE4c1347e172b1: moved over material from AFP; most importantly on algebraic numbers and… | | Mar 30 2024, 12:53 PM |
| pruvisto | rAFP759e3bb5a93e: adapted to isabelle/4c1347e172b1 | | Mar 30 2024, 12:53 PM |
| pruvisto | rAFP759e3bb5a93e: adapted to isabelle/4c1347e172b1 | | Mar 30 2024, 12:52 PM |
| Fabian Huch <huch@in.tum.de> | rAFP36cf00eeb9e4: moved web_app to distribution (see Isabelle/37ea0727291f); | | Mar 30 2024, 1:13 AM |
| Fabian Huch <huch@in.tum.de> | rISABELLEf82639fe786e: update NEWS; | | Mar 30 2024, 1:12 AM |
| Fabian Huch <huch@in.tum.de> | rISABELLE37ea0727291f: moved web_app module from AFP (e.g., for building web services for the… | | Mar 30 2024, 1:08 AM |
| Fabian Huch <huch@in.tum.de> | rAFPe95075447ef6: tuned; | | Mar 30 2024, 1:02 AM |
| Fabian Huch <huch@in.tum.de> | rAFPd95b0fa0cbf5: clarified web app parameters; | | Mar 30 2024, 12:25 AM |
| pruvisto | rAFP52c5d242c69f: sitegen for Doob_Convergence | | Mar 29 2024, 10:51 PM |
| pruvisto | rAFP6d0634427821: new entry Doob_Convergence | | Mar 29 2024, 10:47 PM |
| pruvisto | rISABELLE4c1347e172b1: moved over material from AFP; most importantly on algebraic numbers and… | | Mar 29 2024, 7:28 PM |
| Fabian Huch <huch@in.tum.de> | rAFP0afb82b8179e: proper topic input validation; | | Mar 29 2024, 6:30 PM |
| Fabian Huch <huch@in.tum.de> | rAFPfad1e73aa9b3: clarified web_app paths: better naming, more operations; | | Mar 29 2024, 5:50 PM |
| Fabian Huch <huch@in.tum.de> | rAFP2da2d86049f3: tuned; | | Mar 29 2024, 5:10 PM |
| Fabian Huch <huch@in.tum.de> | rAFPa821024e3b0d: clarified afp_submit: moved submission logic to model; | | Mar 29 2024, 5:08 PM |