| Author | Object | Transaction | Date |
|---|
| Julian Brunner <julianbrunner@gmail.com> | rAFPfe4bf27391fd: generalized degeneralization | | Feb 8 2020, 8:48 PM |
| makarius | rISABELLE5d5be87330b5: allow to override repository versions at runtime; | | Feb 8 2020, 3:18 PM |
| makarius | rISABELLE5de8c6d92bd0: follow Phabricator update 2020 Week 5; | | Feb 7 2020, 8:26 PM |
| florian.haftmann | rISABELLE572ab9e64e18: simplified logical constructions | | Feb 5 2020, 9:17 PM |
| florian.haftmann | rISABELLE1d8e914e04d6: simplified logical constructions | | Feb 5 2020, 9:16 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE89d05db6dd1f: Simplified, generalised version of Constructible due to E. Gunther, M. Pagano… | | Feb 4 2020, 5:19 PM |
| nipkow | rISABELLE6a1c1d1ce6ae: tuned | | Feb 4 2020, 4:36 PM |
| florian.haftmann | rISABELLEbd9d27ccb3a3: more theorems | | Feb 3 2020, 9:42 PM |
| nipkow | rISABELLE63b2789259e7: tuned | | Feb 3 2020, 6:22 PM |
| Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> | rAFPf45e96908c95: Tobias Nipkow found the issue. A line in the proof of frechet_vec_nth. Reduced… | | Feb 3 2020, 5:26 PM |
| Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> | rAFP2002acaf36cc: jenkins/job/isabelle-all still reports fail to build because of timeout. Tested… | | Feb 3 2020, 4:51 PM |
| nipkow | rISABELLEc26de1bd7b00: added Interval_Tree.thy | | Feb 3 2020, 4:49 PM |
| Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> | rAFP61c386d0635b: Increased timeout in ROOT file to avoid fails while building the entry. | | Feb 3 2020, 2:58 PM |
| Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> | rAFP6037ad2499b0: Added a couple of lemmas to shorten proofs for convergence in types of class… | | Feb 3 2020, 1:23 PM |
| Asta Halkjær From <s144442@student.dtu.dk> | rAFPe0ffeae3b9c3: Fix inaccurate word choice. | | Feb 3 2020, 12:47 PM |
| paulson <lp15@cam.ac.uk> | rAFP890686fa8418: type class "small" inclusions for types "set", "real" and "complex" | | Feb 2 2020, 5:23 PM |
| florian.haftmann | rISABELLE65ffe9e910d4: more specific class assumptions | | Feb 1 2020, 7:10 PM |
| florian.haftmann | rISABELLE96d126844adc: more theorems | | Feb 1 2020, 7:10 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFPec727bc82521: added path automata | | Jan 31 2020, 5:43 PM |
| nipkow | rAFP6303a7ad1291: New entry Subset_Boolean_Algebras | | Jan 31 2020, 12:13 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFP2da0b337b200: renaming | | Jan 31 2020, 1:00 AM |
| Julian Brunner <julianbrunner@gmail.com> | rAFPbb9ca3026763: cleanup | | Jan 31 2020, 12:38 AM |
| Julian Brunner <julianbrunner@gmail.com> | rAFP7b3db2da4005: removed unneeded traces | | Jan 30 2020, 10:49 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFP35132c29d428: generalized acceptance test | | Jan 30 2020, 10:21 PM |
| paulson <lp15@cam.ac.uk> | rAFP8a97181d7212: More lemmas, especially about cardinals and the Aleph sequence | | Jan 30 2020, 4:59 PM |
| paulson <lp15@cam.ac.uk> | rAFP637ea3b47f8c: Fixed a failing proof. | | Jan 29 2020, 5:47 PM |
| makarius | rISABELLEfd5cd1daf6a9: build in $ISABELLE_HOME; | | Jan 28 2020, 8:28 PM |
| makarius | rISABELLE91d5a8255c98: build in $ISABELLE_HOME; | | Jan 28 2020, 8:28 PM |
| makarius | rISABELLE839bf7d74fae: ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9); | | Jan 28 2020, 8:28 PM |
| makarius | rISABELLE839bf7d74fae: ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9); | | Jan 28 2020, 8:26 PM |
| paulson <lp15@cam.ac.uk> | rAFPd02b36b86039: ZFC_in_HOL Change history | | Jan 28 2020, 5:51 PM |
| paulson | rAFP6081d5be8d08: merged | | Jan 28 2020, 5:50 PM |
| paulson <lp15@cam.ac.uk> | rAFP589397f68871: Generalisation of order types to arbitrary sets; ordinal exponentiation | | Jan 28 2020, 5:50 PM |
| Alexander Bentkamp <a.bentkamp@vu.nl> | rAFPb2241741f50f: fix imports | | Jan 28 2020, 4:57 PM |
| Alexander Bentkamp <a.bentkamp@vu.nl> | rAFPce989c675f3a: move lemma less_multiset_doubletons | | Jan 28 2020, 4:48 PM |
| paulson | rAFP85592c2f97b1: merged | | Jan 28 2020, 4:15 PM |
| paulson <lp15@cam.ac.uk> | rAFP7393315c7b60: Generalisation of the "small" predicate to arbitrary sets; | | Jan 28 2020, 4:14 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE5385de42f9f4: Tidied up some messy proofs | | Jan 28 2020, 3:59 PM |
| Alexander Bentkamp <a.bentkamp@vu.nl> | rAFPdc7cc57f1157: Lambda-free orders: restrict totality to one set | | Jan 28 2020, 11:22 AM |
| Alexander Bentkamp <a.bentkamp@vu.nl> | rAFP766bfc31745e: merge | | Jan 28 2020, 10:34 AM |
| paulson <lp15@cam.ac.uk> | rISABELLE3ab52e4a8b45: Two lemmas about nsets | | Jan 27 2020, 3:58 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEf2b783abfbe7: A few lemmas connected with orderings | | Jan 27 2020, 3:32 PM |
| nipkow | rAFPddbab58b4c7d: simplified proofs | | Jan 27 2020, 8:47 AM |
| florian.haftmann | rISABELLE554385d4cf59: more theorems | | Jan 26 2020, 9:35 PM |
| florian.haftmann | rISABELLE0bb0cb558bf9: sketches of ideas still to come | | Jan 26 2020, 9:35 PM |
| florian.haftmann | rISABELLE2525e28e4b8b: generalized | | Jan 26 2020, 9:35 PM |
| florian.haftmann | rISABELLE3887432720a9: tuned | | Jan 26 2020, 9:35 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFPa3d250c96907: added union nodes and finiteness theorems | | Jan 24 2020, 4:08 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFP97558303a643: added NBA n-ary union | | Jan 24 2020, 3:30 PM |
| Alexander Bentkamp <a.bentkamp@vu.nl> | rAFP8cbd1aadff7c: EPO: adapt totality proof to suit paper | | Jan 24 2020, 10:58 AM |
| florian.haftmann | rISABELLE43c2355648d2: tuned | | Jan 22 2020, 8:17 PM |
| florian.haftmann | rISABELLEfb9edfe035e1: tuned | | Jan 22 2020, 8:17 PM |
| florian.haftmann | rISABELLEa3ae93ed7b1b: dropped dead code | | Jan 22 2020, 8:17 PM |
| nipkow | rISABELLE58ddd7c5c84e: merged | | Jan 22 2020, 3:23 PM |
| nipkow | rISABELLEa77a3506548d: added lemma | | Jan 22 2020, 2:37 PM |
| pruvisto | rAFP0f0adba767a3: adapted to isabelle-dev/e0237f2eb49d | | Jan 21 2020, 11:55 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFP8b6582b73697: merged | | Jan 21 2020, 5:03 PM |
| Julian Brunner <julianbrunner@gmail.com> | rAFP8e4020889297: added n-ary NBA intersection | | Jan 21 2020, 2:27 PM |
| nipkow | rAFP59346dcf3ea8: finally understood that the second implementation is just a very slight… | | Jan 21 2020, 2:02 PM |
| pruvisto | rISABELLEe0237f2eb49d: Removed multiplicativity assumption from normalization_semidom | | Jan 21 2020, 11:02 AM |
| paulson <lp15@cam.ac.uk> | rAFP11ff77e058c4: webpage for Mersenne_Primes | | Jan 20 2020, 3:36 PM |
| paulson <lp15@cam.ac.uk> | rAFPcd30610ccf05: new entry Mersenne_Primes | | Jan 20 2020, 3:31 PM |
| makarius | rISABELLE028edb1e5b99: clarified file names; | | Jan 19 2020, 2:50 PM |
| makarius | rISABELLEc1c61d0d8e7c: clarified build_polyml_component: include IDE entry point for ML compiler; | | Jan 19 2020, 2:23 PM |
| makarius | rISABELLEd7f8ee80ad42: merged | | Jan 19 2020, 12:57 PM |
| dcjm | rPOLYML5237b653aa69: Rename Root.ML to avoid possible conflict with ROOT.ML in Isabelle. | | Jan 19 2020, 9:10 AM |
| traytel | rISABELLEfce780f9c9c6: new examples of BNF lifting across quotients using a new theory of confluence, | | Jan 19 2020, 7:50 AM |
| dcjm | rPOLYMLf5b8283a1a19: Remove unused variable. This should have been removed in commit 889f7c37. | | Jan 18 2020, 6:53 PM |
| dcjm | rPOLYML889f7c37bc8f: Fix bug with Word.andb(0w0, x). It was wrongly returning "x" rather than zero. | | Jan 18 2020, 6:53 PM |
| dcjm | rPOLYMLf5b8283a1a19: Remove unused variable. This should have been removed in commit 889f7c37. | | Jan 18 2020, 5:03 PM |
| dcjm | rPOLYMLabb79876106c: Fix case problem in one entry. | | Jan 18 2020, 4:47 PM |
| pruvisto | rISABELLEa3f7f00b4fd8: Removed unnecessary and problematic trivial lemma from HOL-Algebra | | Jan 17 2020, 6:58 PM |
| pruvisto | rAFP1775f91f0787: Fixed broken citation in Poincare_Disc | | Jan 17 2020, 6:48 PM |
| makarius | rISABELLE933ad2385480: tuned spelling; | | Jan 17 2020, 4:59 PM |
| pruvisto | rAFPa4ca8d95843b: fixed incorrect HTML entity in Poincare_Disc metadata | | Jan 17 2020, 4:33 PM |
| pruvisto | rAFPa222e106ac18: added new entries: Complex_Geometry and Poincare_Disc | | Jan 17 2020, 4:25 PM |
| makarius | rISABELLE5556ae257df9: proper executable file; | | Jan 16 2020, 5:04 PM |
| nipkow | rAFPd7cc55445292: tuned topics | | Jan 16 2020, 4:53 PM |
| makarius | rISABELLE5e7ba6aa85d7: more documentation: odd option for special situations; | | Jan 16 2020, 4:41 PM |
| makarius | rISABELLE21995f5e8126: tuned; | | Jan 16 2020, 4:35 PM |
| makarius | rISABELLE57861bd0a3e1: updated to sumatra_pdf-3.1.2-1: x86_64-windows; | | Jan 16 2020, 4:15 PM |
| makarius | rISABELLEb3b992f6ad8f: updated to stack-2.1.3, stackage lts-13.19, ghc-8.6.4; | | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | makarius created this object with edit policy "Task Author". | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | makarius created this object with visibility "Public (No Login Required)". | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | makarius triaged this task as Low priority. | Jan 16 2020, 4:07 PM |
| makarius | T11: HOL-Quickcheck_Examples fails on Windows | | Jan 16 2020, 4:07 PM |
| makarius | rISABELLEb3b992f6ad8f: updated to stack-2.1.3, stackage lts-13.19, ghc-8.6.4; | | Jan 16 2020, 3:34 PM |
| makarius | rISABELLE7e8e5e1f8f90: updated to opam-2.0.6; | | Jan 16 2020, 3:10 PM |
| makarius | rISABELLE06bb82e7af2a: updated to current cygwin, after 3.1.2-1 from 21-Dec-2019; | | Jan 16 2020, 2:07 PM |
| paulson <lp15@cam.ac.uk> | rAFPc0d0d29ff0e7: Approximation_Algorithms website | | Jan 16 2020, 12:55 PM |
| paulson <lp15@cam.ac.uk> | rAFPe1ade233ba62: new entry Approximation_Algorithms | | Jan 16 2020, 12:52 PM |
| makarius | T10: Font rendering quality in OpenJDK 11 vs. 17 | makarius created this object with visibility "Public (No Login Required)". | Jan 16 2020, 12:08 PM |
| makarius | T10: Font rendering quality in OpenJDK 11 vs. 17 | | Jan 16 2020, 12:08 PM |
| makarius | T10: Font rendering quality in OpenJDK 11 vs. 17 | makarius created this object with edit policy "Task Author". | Jan 16 2020, 12:08 PM |
| makarius | T10: Font rendering quality in OpenJDK 11 vs. 17 | | Jan 16 2020, 12:08 PM |
| makarius | T10: Font rendering quality in OpenJDK 11 vs. 17 | makarius triaged this task as Low priority. | Jan 16 2020, 12:08 PM |