Page MenuHomeIsabelle/Phabricator
Feed All Stories

Jan 24 2023

Fabian Huch <huch@in.tum.de> committed rAFP218f8b36e463: tuned css;.
tuned css;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP8c56f5c6b995: cleanup accidental unused document files;.
cleanup accidental unused document files;
Jan 24 2023, 12:35 PM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPf71500561ddd: new entry StrictOmegaCategories.
new entry StrictOmegaCategories
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP2eadd58953b2: tuned css;.
tuned css;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFPb6e17fba3920: tuned;.
tuned;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP8f3963fc318e: check ROOTs: add warning-only checks;.
check ROOTs: add warning-only checks;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFPbe286bc20358: add ROOT checks for document presence and unused files;.
add ROOT checks for document presence and unused files;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFPe1994f6b8765: update bibtex example;.
update bibtex example;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFPcf0f60410d41: afp-submit visual improvements;.
afp-submit visual improvements;
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP5ed170d26665: sitegen for AOT.
sitegen for AOT
Jan 24 2023, 12:35 PM
nipkow committed rAFP086e65efb46c: New entry: Propositional_Logic_Class.
New entry: Propositional_Logic_Class
Jan 24 2023, 12:35 PM
paulson committed rAFPd3f9882dd945: merged.
merged
Jan 24 2023, 12:35 PM
nipkow committed rAFPa323d2b37bbe: new doi.
new doi
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP82485f4069a3: sitegen for Cook_Levin.
sitegen for Cook_Levin
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP757cd45633e5: New entry AOT.
New entry AOT
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFPfd1706186cfd: Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious….
Metadata for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Boolos_Curious…
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP15cc700782ed: New entry Cook_Levin.
New entry Cook_Levin
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP30d87b385d1b: Sorry — extra files for Boolos_Curious_Inference_Automated.
Sorry — extra files for Boolos_Curious_Inference_Automated
Jan 24 2023, 12:35 PM
nipkow committed rAFPe33b36de67b6: New entry: Synthetic_Completeness.
New entry: Synthetic_Completeness
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFPffdd481ec642: New entry Boolos_Curious_Inference_Automated.
New entry Boolos_Curious_Inference_Automated
Jan 24 2023, 12:35 PM
nipkow committed rAFP77385ec30deb: New entry Birkhoff_Finite_Distributive_Lattices.
New entry Birkhoff_Finite_Distributive_Lattices
Jan 24 2023, 12:35 PM
nipkow committed rAFP81dc779aa4f6: New entry: Quantifier_Elimination_Hybrid.
New entry: Quantifier_Elimination_Hybrid
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP448ffe79d636: sitegen for Kneser_Cauchy_Davenport.
sitegen for Kneser_Cauchy_Davenport
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2202fa913caa: sitegen for Turan.
sitegen for Turan
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP784beb76e81b: metadata for Kneser_Cauchy_Davenport.
metadata for Kneser_Cauchy_Davenport
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP5afdc1fb29fe: new entry: Kneser_Cauchy_Davenport.
new entry: Kneser_Cauchy_Davenport
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2e81f7e68084: added metadata for Turans graph theorem.
added metadata for Turans graph theorem
Jan 24 2023, 12:35 PM
kleing committed rAFP64c2e9afb33f: new entry Multitape_To_Singletape_TM.
new entry Multitape_To_Singletape_TM
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPedfa39d8f358: new entry: Turans Graph Theorem.
new entry: Turans Graph Theorem
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP9d7a4bb4c4c7: removed static pages from rss feed;.
removed static pages from rss feed;
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFPe4b0db223808: sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Le….
sitegen for /Users/lp15/.isabelle/Isabelle2022/browser_info/AFP/Sauer_Shelah_Le…
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP962b39db2ea2: New entry Sauer_Shelah_Lemma.
New entry Sauer_Shelah_Lemma
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP7ad5b3b42714: Minor rerating of the abstract of Sauer_Shelah_Lemma.
Minor rerating of the abstract of Sauer_Shelah_Lemma
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP744bc08e5559: sitegen for the aforementioned changes.
sitegen for the aforementioned changes
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFPe32f62f09a5c: CHERI-C_Memory_Model patch & metadata.
CHERI-C_Memory_Model patch & metadata
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFP859ca93a6501: New submission CHERI-C_Memory_Model.
New submission CHERI-C_Memory_Model
Jan 24 2023, 12:35 PM
paulson <lp15@cam.ac.uk> committed rAFPa289908c1dc9: adjustments to the abstract, requested by the author.
adjustments to the abstract, requested by the author
Jan 24 2023, 12:35 PM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP3d36623c6b42: metadata and sitegen for PAPP_Impossibility.
metadata and sitegen for PAPP_Impossibility
Jan 24 2023, 12:35 PM
pruvisto committed rAFP3c9c4cbba508: fixed broken abstract for PAPP_Impossibility.
fixed broken abstract for PAPP_Impossibility
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFPc35d3a21bdeb: updated docs;.
updated docs;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP05fbf155c600: improve page layout slightly;.
improve page layout slightly;
Jan 24 2023, 12:35 PM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPe847e0ae6e76: remove dead code.
remove dead code
Jan 24 2023, 12:35 PM
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP19511710a590: new entry PAPP_Impossibility.
new entry PAPP_Impossibility
Jan 24 2023, 12:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP43822ae262d7: metadata and sitegen for Balog_Szemeredi_Gowers.
metadata and sitegen for Balog_Szemeredi_Gowers
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP7c35ca18de56: remove old .sitegen-ignore and mention AFP chapter in submission guidelines;.
remove old .sitegen-ignore and mention AFP chapter in submission guidelines;
Jan 24 2023, 12:35 PM
Fabian Huch <huch@in.tum.de> committed rAFP574e7b39ce67: afp_check_roots: proper error message printing;.
afp_check_roots: proper error message printing;
Jan 24 2023, 12:34 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP91090ec4049a: new entry: Balog_Szemeredi_Gowers.
new entry: Balog_Szemeredi_Gowers
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPf884fa0d7a78: make check roots tool less dependent on AFP structure;.
make check roots tool less dependent on AFP structure;
Jan 24 2023, 12:34 PM
nipkow committed rAFP281f4207a7e7: web for Combinatorial_Enumeration_Algorithms.
web for Combinatorial_Enumeration_Algorithms
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPa6457a3f85d8: tuned check names;.
tuned check names;
Jan 24 2023, 12:34 PM
nipkow committed rAFP637b3599cda6: sitegen for Combinatorial_Enumeration_Algorithms.
sitegen for Combinatorial_Enumeration_Algorithms
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP1c7dbae922fd: tuned;.
tuned;
Jan 24 2023, 12:34 PM
nipkow committed rAFPf83f530c4b47: New entry Combinatorial_Enumeration_Algorithms.
New entry Combinatorial_Enumeration_Algorithms
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP8668822cee79: fix duplicate affiliations from author and notify;.
fix duplicate affiliations from author and notify;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPdea38bffa477: check for entries instead of session due to session nesting allowed in entries;.
check for entries instead of session due to session nesting allowed in entries;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP3c67738ceaa2: add metadata check tool to sitegen;.
add metadata check tool to sitegen;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP86c85aea4b83: added unused thy check;.
added unused thy check;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP08c77145d2d4: update check tools: add formatting checks, new cmd options;.
update check tools: add formatting checks, new cmd options;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPca43dc336328: afp-submit: tuned logging;.
afp-submit: tuned logging;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP253533a603e3: afp-submit: encode new notify addresses properly;.
afp-submit: encode new notify addresses properly;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP43503a55dbad: clarified check roots tool;.
clarified check roots tool;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPe8b08d471fc8: re-format metadata;.
re-format metadata;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP1ae3c6cfde77: afp-submit: remove padding on select;.
afp-submit: remove padding on select;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP7d8e3591aa0d: afp-submit: correct build status on empty file;.
afp-submit: correct build status on empty file;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP1885292283fe: afp-submit: update on correct status change;.
afp-submit: update on correct status change;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPaa91117e48cf: afp-submit: clarified date format, tuned logging;.
afp-submit: clarified date format, tuned logging;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP164aa0056a2d: switch fonts to www prefixed isa-afp.org domain;.
switch fonts to www prefixed isa-afp.org domain;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPabfd82b150f6: clarified afp-submit error handling;.
clarified afp-submit error handling;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFP2f4e11acf6a0: switch to www prefixed isa-afp.org domain;.
switch to www prefixed isa-afp.org domain;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPa7f664314a45: clarified afp-submit creation and message;.
clarified afp-submit creation and message;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPa338559ef142: list submission system website;.
list submission system website;
Jan 24 2023, 12:34 PM
Fabian Huch <huch@in.tum.de> committed rAFPc7ba56881098: afp-submit: clarified api urls;.
afp-submit: clarified api urls;
Jan 24 2023, 12:34 PM
florian.haftmann committed rISABELLE5de3772609ea: generalized theory name: euclidean division denotes one particular division….
generalized theory name: euclidean division denotes one particular division…
Jan 24 2023, 12:00 PM
florian.haftmann committed rAFPdb93f67adfd0: generalized theory name: euclidean division denotes one particular division….
generalized theory name: euclidean division denotes one particular division…
Jan 24 2023, 12:00 PM
florian.haftmann committed rAFP75e99d0e6664: more efficient specification.
more efficient specification
Jan 24 2023, 12:00 PM

Jan 23 2023

makarius committed rISABELLE44f79689115d: more elementary command-line, following lib/Tools/components;.
more elementary command-line, following lib/Tools/components;
Jan 23 2023, 11:36 PM
makarius committed rISABELLEa5d3f3c07de8: merged.
merged
Jan 23 2023, 11:36 PM
makarius committed rISABELLE422c57b75b17: support remote operations;.
support remote operations;
Jan 23 2023, 11:36 PM
makarius committed rISABELLEf56800b8b085: clarified defaults;.
clarified defaults;
Jan 23 2023, 11:36 PM
makarius committed rISABELLEf60dd8d76515: more accurate options (amending 7e19dc018db9);.
more accurate options (amending 7e19dc018db9);
Jan 23 2023, 11:36 PM
makarius committed rISABELLEe233054dcb00: clarified defaults;.
clarified defaults;
Jan 23 2023, 11:36 PM
makarius committed rISABELLEc839b84ee66f: more modular shell script;.
more modular shell script;
Jan 23 2023, 11:36 PM
makarius committed rISABELLE3bb374ac31b3: support remote download_file;.
support remote download_file;
Jan 23 2023, 11:36 PM
makarius committed rISABELLEe57ba228ec24: tuned: drop redundant "expand";.
tuned: drop redundant "expand";
Jan 23 2023, 11:36 PM
makarius committed rISABELLE86ace3c45837: more uniform options for "curl", following lib/Tools/components;.
more uniform options for "curl", following lib/Tools/components;
Jan 23 2023, 11:36 PM
makarius committed rISABELLE92509e4274eb: tuned;.
tuned;
Jan 23 2023, 11:36 PM
desharna committed rISABELLEe293216df994: added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp.
added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp
Jan 23 2023, 7:34 PM
desharna committed rISABELLE1c358879bfd3: proper name for lemma totalp_on_total_on_eq.
proper name for lemma totalp_on_total_on_eq
Jan 23 2023, 7:34 PM
paulson <lp15@cam.ac.uk> committed rAFP95ab3b6c963f: Removal of more unused material.
Removal of more unused material
Jan 23 2023, 6:10 PM
paulson <lp15@cam.ac.uk> committed rAFPc8f289838f39: Small simplifications. Removed a needless assumption..
Small simplifications. Removed a needless assumption.
Jan 23 2023, 5:55 PM
makarius committed rISABELLE39f8051f71d4: update to jdk-17.0.6;.
update to jdk-17.0.6;
Jan 23 2023, 12:05 AM
makarius committed rISABELLEf51b0b54b20b: avoid odd suffix in published HTML library;.
avoid odd suffix in published HTML library;
Jan 23 2023, 12:05 AM
makarius committed rISABELLE671ca79e2644: proper cleanup;.
proper cleanup;
Jan 23 2023, 12:05 AM

Jan 22 2023

makarius committed rISABELLEdaf13aec9f04: tuned message;.
tuned message;
Jan 22 2023, 10:29 PM
makarius committed rISABELLEa4380a2d6d2c: tuned signature: avoid aliases;.
tuned signature: avoid aliases;
Jan 22 2023, 10:29 PM
makarius committed rISABELLE67da045668cc: tuned;.
tuned;
Jan 22 2023, 10:29 PM
makarius committed rISABELLE4adee07a5e48: tuned signature;.
tuned signature;
Jan 22 2023, 10:29 PM
makarius committed rISABELLE96879e303ea3: clarified modules (again, in contrast to f8f065e20837);.
clarified modules (again, in contrast to f8f065e20837);
Jan 22 2023, 10:29 PM
makarius committed rISABELLE2f09dc0e6dda: support IPC via database server;.
support IPC via database server;
Jan 22 2023, 9:46 PM
makarius committed rISABELLE7b5b1789a34c: proper signature;.
proper signature;
Jan 22 2023, 9:46 PM