Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
makariusrISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to…Apr 2 2024, 7:32 PM
makariusrISABELLEd67cacd09251: mergedApr 2 2024, 7:18 PM
Lars Hupel <lars@hupel.info>rAFP0d5e63bc2b19: merged
Lars Hupel <lars@hupel.info> committed rAFP0d5e63bc2b19: merged. 
Apr 2 2024, 7:11 PM
makariusrISABELLE09e9819beef6: update to stack-2.15.5, stackage-lts-22.15;Apr 2 2024, 7:10 PM
makariusrISABELLE951c371c1cd9: clarified names: discontinue odd convention from 3 decades ago;Apr 2 2024, 6:29 PM
pruvistorISABELLE33a9b1d6a651: added documentation for meromorphicity etc. in HOL-Complex_AnalysisApr 2 2024, 6:02 PM
makariusrISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to…Apr 2 2024, 5:20 PM
desharnarAFP424dc98e93ad: adapted to Isabelle/67e77f1e6d7bApr 2 2024, 4:34 PM
desharnarISABELLE67e77f1e6d7b: added special syntax for FSet.Ball and FSet.BexApr 2 2024, 4:34 PM
desharnarISABELLE876bb57e7376: merged
desharna committed rISABELLE876bb57e7376: merged. 
Apr 2 2024, 4:33 PM
desharnarAFP424dc98e93ad: adapted to Isabelle/67e77f1e6d7bApr 2 2024, 4:33 PM
makariusrAFP5819f2a448d6: tuned proofs: avoid z3 to make it work on arm64-linux;Apr 2 2024, 2:53 PM
traytelrAFP51fb7da70175: sitegen for Broadcast_PsiApr 2 2024, 2:34 PM
traytelrAFP31ea85757858: new entry Broadcast_PsiApr 2 2024, 1:29 PM
Lars Hupel <lars@hupel.info>rAFPa8ac72f7dd9f: make Go test mandatory
Lars Hupel <lars@hupel.info> committed rAFPa8ac72f7dd9f: make Go test mandatory. 
Apr 2 2024, 11:51 AM
Lars Hupel <lars@hupel.info>rAFP985b115c06a9: remove generated files
Lars Hupel <lars@hupel.info> committed rAFP985b115c06a9: remove generated files. 
Apr 2 2024, 11:42 AM
Lars Hupel <lars@hupel.info>rISABELLEd6a787ccf583: remove transitional (dummy) component list for GoApr 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
desharnarISABELLE6de94d690f9f: merged
desharna committed rISABELLE6de94d690f9f: merged. 
Apr 2 2024, 8:35 AM
makariusrAFPc99fa2f32389: tuned proofs: avoid z3 to make it work on arm64-linux;Apr 1 2024, 10:33 PM
makariusrAFP4034bbbba794: tuned proofs: avoid z3 to make it work on arm64-linux;Apr 1 2024, 9:34 PM
makariusrAFPde38656982c3: tuned whitespace;Apr 1 2024, 7:13 PM
makariusrISABELLE9c00a46d69d0: new simplifier trace_op for tracing simproc callsApr 1 2024, 7:06 PM
makariusrISABELLEc5cd7a58cf2d: generic trace operations for main steps of Simplifier;Apr 1 2024, 7:06 PM
makariusrISABELLE0d94dd2fd2d0: clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);Apr 1 2024, 7:06 PM
makariusrISABELLE06153e2e0cdb: more official AFP.groups;Apr 1 2024, 7:06 PM
makariusrISABELLE1478c6d52864: clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that…Apr 1 2024, 7:06 PM
makariusrAFP0c06ebfbaba1: tuned proofs: avoid z3 to make it work on arm64-linux;Apr 1 2024, 6:46 PM
makariusrAFPc1af731e14b9: tuned proofs: avoid z3 to make it work on arm64-linux;Apr 1 2024, 6:46 PM
makariusrISABELLE60b6c735b5d5: clarified signature: prefer authentic cterm used in Simplifier, avoid potential…Apr 1 2024, 3:47 PM
makariusrISABELLE0d94dd2fd2d0: clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);Apr 1 2024, 3:37 PM
makariusrISABELLE588ea80f16bb: provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;Apr 1 2024, 3:09 PM
makariusrISABELLE1478c6d52864: clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that…Apr 1 2024, 2:36 PM
pruvistorAFP1cd8d5cb1636: adapted Zeta_3_Irrational w.r.t. isabelle/4c1347e172b1Mar 30 2024, 9:18 PM
pruvistorISABELLE4c1347e172b1: moved over material from AFP; most importantly on algebraic numbers and…Mar 30 2024, 9:18 PM
pruvistorAFP1cd8d5cb1636: adapted Zeta_3_Irrational w.r.t. isabelle/4c1347e172b1Mar 30 2024, 9:17 PM
pruvistorISABELLE4c1347e172b1: moved over material from AFP; most importantly on algebraic numbers and…Mar 30 2024, 12:53 PM
pruvistorAFP759e3bb5a93e: adapted to isabelle/4c1347e172b1Mar 30 2024, 12:53 PM
pruvistorAFP759e3bb5a93e: adapted to isabelle/4c1347e172b1Mar 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;
Fabian Huch <huch@in.tum.de> committed 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;
Fabian Huch <huch@in.tum.de> committed rAFPe95075447ef6: tuned;. 
Mar 30 2024, 1:02 AM
Fabian Huch <huch@in.tum.de>rAFPd95b0fa0cbf5: clarified web app parameters;
Fabian Huch <huch@in.tum.de> committed rAFPd95b0fa0cbf5: clarified web app parameters;. 
Mar 30 2024, 12:25 AM
pruvistorAFP52c5d242c69f: sitegen for Doob_ConvergenceMar 29 2024, 10:51 PM
pruvistorAFP6d0634427821: new entry Doob_ConvergenceMar 29 2024, 10:47 PM
pruvistorISABELLE4c1347e172b1: 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;
Fabian Huch <huch@in.tum.de> committed 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;
Fabian Huch <huch@in.tum.de> committed 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
Fabian Huch <huch@in.tum.de>rAFP2c7c46f5b86b: clarified afp_submit: separate model, view, and (API) paths properly;Mar 29 2024, 3:53 PM
Fabian Huch <huch@in.tum.de>rAFPfbd3048e5c19: better rendering of submission archive and Isabelle log;Mar 29 2024, 2:12 PM
paulson <lp15@cam.ac.uk>rAFPb87e29fd506a: sitegen for Kummer_Congruence
paulson <lp15@cam.ac.uk> committed rAFPb87e29fd506a: sitegen for Kummer_Congruence. 
Mar 29 2024, 1:40 PM
paulson <lp15@cam.ac.uk>rAFP1ebd4536fe74: New entry Kummer_Congruence
paulson <lp15@cam.ac.uk> committed rAFP1ebd4536fe74: New entry Kummer_Congruence. 
Mar 29 2024, 1:37 PM
paulson <lp15@cam.ac.uk>rAFPceff43a60f39: sitegen for CondNormReasHOL
paulson <lp15@cam.ac.uk> committed rAFPceff43a60f39: sitegen for CondNormReasHOL. 
Mar 29 2024, 1:20 PM
paulson <lp15@cam.ac.uk>rAFP5f12b29d4a50: New entry CondNormReasHOL
paulson <lp15@cam.ac.uk> committed rAFP5f12b29d4a50: New entry CondNormReasHOL. 
Mar 29 2024, 1:10 PM
Eugene W. Stark <stark@cs.stonybrook.edu>rAFP449ac450b3a6: Merged.
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP449ac450b3a6: Merged.. 
Mar 29 2024, 2:58 AM
Eugene W. Stark <stark@cs.stonybrook.edu>rAFP6610630663ea: Sync with my development repo.
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP6610630663ea: Sync with my development repo.. 
Mar 29 2024, 2:57 AM
Fabian Huch <huch@in.tum.de>rAFPc59ea7fd010b: proper state handling in submission handler;
Fabian Huch <huch@in.tum.de> committed rAFPc59ea7fd010b: proper state handling in submission handler;. 
Mar 29 2024, 12:24 AM
Fabian Huch <huch@in.tum.de>rAFP28ad1f400df1: tuned;
Fabian Huch <huch@in.tum.de> committed rAFP28ad1f400df1: tuned;. 
Mar 29 2024, 12:23 AM
Fabian Huch <huch@in.tum.de>rAFP5fcf885cecfd: tuned name;
Fabian Huch <huch@in.tum.de> committed rAFP5fcf885cecfd: tuned name;. 
Mar 29 2024, 12:13 AM
Fabian Huch <huch@in.tum.de>rAFP519c2c73b80e: add explicit synchronized server state;
Fabian Huch <huch@in.tum.de> committed rAFP519c2c73b80e: add explicit synchronized server state;. 
Mar 28 2024, 7:37 PM
Fabian Huch <huch@in.tum.de>rAFP45bd80541bcd: more uniform load_entries;
Fabian Huch <huch@in.tum.de> committed rAFP45bd80541bcd: more uniform load_entries;. 
Mar 28 2024, 7:26 PM
Fabian Huch <huch@in.tum.de>rAFP7a425b5f62ba: tuned: prefer for-comprehension in complicated situations;Mar 28 2024, 6:48 PM
Fabian Huch <huch@in.tum.de>rAFPb93b79b9240e: tuned formatting;
Fabian Huch <huch@in.tum.de> committed rAFPb93b79b9240e: tuned formatting;. 
Mar 28 2024, 6:30 PM
Fabian Huch <huch@in.tum.de>rAFP01987db5d362: tuned: more uniform Isabelle style;
Fabian Huch <huch@in.tum.de> committed rAFP01987db5d362: tuned: more uniform Isabelle style;. 
Mar 28 2024, 6:25 PM
Emin Karayel <me@eminkarayel.de>rAFPf8eca525e197: Distributed_Distinct_Elements: Fix aliasing issue introduce in isabelle…Mar 28 2024, 6:14 PM
Fabian Huch <huch@in.tum.de>rAFPf111b9c197e8: tuned imports;
Fabian Huch <huch@in.tum.de> committed rAFPf111b9c197e8: tuned imports;. 
Mar 28 2024, 5:56 PM
makariusrAFP0df87a34e8a0: mergedMar 28 2024, 5:45 PM
Fabian Huch <huch@in.tum.de>rAFPb7690d847464: tuned;
Fabian Huch <huch@in.tum.de> committed rAFPb7690d847464: tuned;. 
Mar 28 2024, 5:44 PM
Fabian Huch <huch@in.tum.de>rAFP307a818fb212: clarified options;
Fabian Huch <huch@in.tum.de> committed rAFP307a818fb212: clarified options;. 
Mar 28 2024, 5:38 PM
makariusrAFP5aca58481bd5: tuned proofs: avoid z3 to make it work on arm64-linux;Mar 28 2024, 5:35 PM
makariusrAFPabe7b3319f06: tuned whitespace;Mar 28 2024, 5:26 PM
makariusrAFP4c396108a3a9: tuned proofs: avoid z3 to make it work on arm64-linux;Mar 28 2024, 5:21 PM
makariusrAFP2c25484e1496: tuned proofs: avoid z3 to make it work on arm64-linux;Mar 28 2024, 4:57 PM
makariusrISABELLE87f90735e6dd: removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g.Mar 28 2024, 4:45 PM
makariusrISABELLEf150253cb201: RDF meta data for AFP entries;Mar 28 2024, 4:45 PM
makariusrISABELLE87f90735e6dd: removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g.Mar 28 2024, 4:40 PM
makariusrISABELLE9279e96eb34e: clarified signature;Mar 28 2024, 4:38 PM
makariusrAFP9ce4d6a809c6: update to Isabelle/42bc8ab751c1;Mar 28 2024, 4:28 PM
makariusrISABELLE42bc8ab751c1: clarified modules: more official Sessions.notable_groups;Mar 28 2024, 4:27 PM
nipkowrISABELLEf8d7df38d7c6: tuned
nipkow committed rISABELLEf8d7df38d7c6: tuned. 
Mar 28 2024, 4:14 PM
Fabian Huch <huch@in.tum.de>rAFP9cad40069322: add option to run formatting operations on all metadata files;Mar 28 2024, 4:07 PM
Fabian Huch <huch@in.tum.de>rISABELLE68f6b29ae066: tuned;
Fabian Huch <huch@in.tum.de> committed rISABELLE68f6b29ae066: tuned;. 
Mar 28 2024, 3:08 PM
Fabian Huch <huch@in.tum.de>rAFP4cb970a0955a: clarified types: richer interface for metadata;Mar 28 2024, 2:47 PM
paulsonrISABELLE44d8fb3da9d5: merged
paulson committed rISABELLE44d8fb3da9d5: merged. 
Mar 28 2024, 2:33 PM
paulson <lp15@cam.ac.uk>rISABELLE35b2143aeec6: An assortment of new material, mostly due to ManuelMar 28 2024, 2:32 PM
makariusrISABELLE9cdc4f533b91: rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;Mar 28 2024, 12:56 PM
Fabian Huch <huch@in.tum.de>rAFP4395ecd3d7a5: tuned;
Fabian Huch <huch@in.tum.de> committed rAFP4395ecd3d7a5: tuned;. 
Mar 28 2024, 12:15 PM
makariusrISABELLE7d8a24c5559d: tuned signature;Mar 28 2024, 11:45 AM
makariusrISABELLEb525f783b784: tuned;Mar 28 2024, 11:35 AM
makariusrISABELLEa213dd3c0b29: tuned signature;Mar 28 2024, 11:29 AM
desharnarISABELLE67e77f1e6d7b: added special syntax for FSet.Ball and FSet.BexMar 28 2024, 9:41 AM
desharnarISABELLE804a41d08b84: tuned proofMar 28 2024, 9:40 AM
desharnarISABELLE19cc354ba625: merged
desharna committed rISABELLE19cc354ba625: merged. 
Mar 28 2024, 8:30 AM
makariusrISABELLE308ccc1ef982: proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;Mar 27 2024, 10:56 PM
makariusrISABELLEda323d3d7570: proper "isabelle go_setup" for Jenkins;Mar 27 2024, 10:35 PM
makariusrAFP1699d5f4b11d: proper Go setup, following Isabelle/da323d3d7570;Mar 27 2024, 10:35 PM
makariusrAFP1699d5f4b11d: proper Go setup, following Isabelle/da323d3d7570;Mar 27 2024, 10:19 PM