quanrong <quanrong@mailbox.org> committed rPOLYML0c6a7c1a7ba5: fromString: remove possible leading zeros in il@fl (authored by quanrong <quanrong@mailbox.org>).

quanrong <quanrong@mailbox.org> committed rPOLYML6389f9b0c0e2: fromString: remove possible trailing zeros in il@fl (authored by quanrong <quanrong@mailbox.org>).

quanrong <quanrong@mailbox.org> committed rPOLYML8cb5a80011ef: Refactor the removing of leading and trailing zeros (authored by quanrong <quanrong@mailbox.org>).

quanrong <quanrong@mailbox.org> committed rPOLYML7c75068a3724: fromString: fix overflow when exponent is too long but base is zero (authored by quanrong <quanrong@mailbox.org>).

quanrong <quanrong@mailbox.org> committed rPOLYML821b3dd8ed17: Fix error in exponent when both leading and trailing are nonempty (authored by quanrong <quanrong@mailbox.org>).

dcjm committed rPOLYML4c4c57712caf: Add a regression test for real scan and fromString. Currently only contains a… (authored by dcjm).

quanrong <quanrong@mailbox.org> committed rPOLYMLbf1f331926d9: Fix exp calculation according to the Basis spec (authored by quanrong <quanrong@mailbox.org>).

dcjm committed rPOLYMLada6599d7835: Define Real.scan and Real.fromString in terms of IEEEReal.scan and IEEEReal. (authored by dcjm).

quanrong <quanrong@mailbox.org> committed rPOLYML5318f518687c: Add clarifying comment (authored by quanrong <quanrong@mailbox.org>).

dcjm committed rPOLYML6c9cac664894: Merge commit '821b3dd8ed17e3a8cefbcc3418f625cf04e215fd' into IEEERealFixes (authored by dcjm).

dcjm committed rPOLYMLf994ab4edfa4: Empty the save-vec at the start of every RTS call. The calls to SaveVec::mark… (authored by dcjm).

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP4b81052d10a7: metadata and sitegen for Directed_Sets.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa75bef9732a0: new entry: Directed_Sets.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPdc5bd1c28e35: merge from AFP 2022.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP4455b9dd5e3f: metadata and sitegen for Multirelations_Heterogeneous.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP3f8f0fe5fef5: new entry: Multirelations_Heterogeneous.

makarius committed rISABELLEb7b777fc916c: Added tag Isabelle2023-RC0 for changeset f4221ae7544c.

makarius created Blog Post: Release Candidates for Isabelle2023.

makarius committed rISABELLE5faedbc01c07: updated to postgresql-42.6.0;.

makarius committed rISABELLEf4221ae7544c: updated to zstd-jni-1.5.5-4;.

makarius committed rISABELLE979036f4f42c: more PLATFORMS;.

makarius committed rISABELLE2a28450b992b: back to more concise build_release, thanks to build_host_macos = "mini3";.

makarius committed rISABELLE7ea4f986e41a: updated for release;.

makarius committed rISABELLEa502d7e06855: tuned NEWS;.

makarius committed rISABELLE456576153249: more realistic factor;.

makarius committed rISABELLE90a43a9b3605: proper trim_context;.

makarius committed rISABELLEbb85bda12b8e: proper exception positions;.

makarius committed rISABELLE0ea55458f867: proper trim_context / transfer, e.g. for Specification.definition;.

makarius committed rISABELLEe1bd2eb4c407: tuned;.

makarius committed rISABELLE9ccb1ae28f0d: tuned;.

makarius committed rISABELLEa11ebc8c751a: minor performance tuning: avoid append to end-of-list;.

makarius committed rISABELLEdb2a6f9aaa77: tuned signature: more operations;.

Yong Kiam Tan <yongkiat@cs.cmu.edu> committed rAFP444e642b5026: adjust Schwartz_Zippel entry.

nipkow committed rISABELLE0a098088745b: TN has enough examples of the bug..

desharna committed rISABELLE177dae28697b: added lemma ffUnion_fsubset_iff.

desharna committed rAFP7ee0aee653f8: adjusted Simple_Clause_Learning from AFP 2022 to AFP devel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb9d25a201574: merge from afp-2022.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP7aa9ab057cd7: adjusted Given_Clause_Loops from AFP 2022 to AFP devel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP7855f111caf9: adjusted DigitsInBase from AFP 2022 to AFP devel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP81a6759dfada: adjusted Schwartz_Zippel from AFP 2022 to AFP devel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb2fa2ad6a242: adjusted CommCSL from AFP 2022 to AFP devel.

nipkow committed rAFP68c085f87ed9: New entry Efficient_Weighted_Path_Order.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPe31ee8403c7b: adjusted efficient WPO from AFP 2022 to afp devel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP58b26f37f4e6: adjusted TsirelsonBound from AFP 2022 to AFP devel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP67fa1b4a62ba: adjusted Tree_Enumeration from AFP 2022 to AFP devel.

Fabian Huch <huch@in.tum.de> committed rAFP2458cc9f2178: add edit mode to afp-submit UI;.

Fabian Huch <huch@in.tum.de> committed rAFPe01c52833656: better error logging;.

Fabian Huch <huch@in.tum.de> committed rAFP86fc101623c5: solved subtle problem with multiple entries and new authors;.

Fabian Huch <huch@in.tum.de> committed rAFP99128d447af7: added frontend in devel mode;.

Fabian Huch <huch@in.tum.de> committed rAFPafff7edfd8b3: tuned (mostly api path handling);.

paulson <lp15@cam.ac.uk> committed rAFPb4d2af04b7eb: MLSS_Decision_Proc sitegen.

paulson <lp15@cam.ac.uk> committed rAFP45762d22cd88: A real title in place of MLSS_Decision_Proc.

Fabian Huch <huch@in.tum.de> committed rAFPf6635b128bb7: added edit handler to submission app;.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd5c2c7bf2e5c: metadata and sitegen for TsirelsonBound.

paulson <lp15@cam.ac.uk> committed rAFP1714e1c24057: New entry MLSS_Decision_Proc.

nipkow committed rAFP8003229c957d: New entry Tree_Enumeration.

paulson <lp15@cam.ac.uk> committed rAFP7f7e0823fad6: Three_Squares citegen.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP9be80c722f4d: new entry: TsirelsonBound.

paulson <lp15@cam.ac.uk> committed rAFPcc5da931919e: New entry Three_Squares.

nipkow committed rAFPeabb29dd60f8: more files.

pruvisto committed rAFPed44e5fe1c91: fixed some ACM/AMS categories.

Fabian Huch <huch@in.tum.de> committed rAFPe184ebea4edb: added new entry DigitsInBase;.

nipkow committed rAFP40e9b3cc3b69: New entry MHComputation.

pruvisto committed rAFP8803006aad0b: fixed broken LaTeX quotation marks in abstracts.

Fabian Huch <huch@in.tum.de> committed rAFPab6622e175b5: cleanup;.

Fabian Huch <huch@in.tum.de> committed rAFPb2618bec65de: make index.json files line-by-line for smaller diffs;.

pruvisto committed rAFP112513d0e2e3: recategorised some entries.

pruvisto committed rAFP34a086c9abed: sitegen for Schwartz_Zippel.

pruvisto committed rAFP4ecd1e3b58a6: new topic: Computer science/Algorithms/Randomized.

nipkow committed rAFP97aa28cdec1a: New entry HyperHoareLogic.

pruvisto committed rAFP4e19c676a55f: new entry: Schwartz_Zippel.

nipkow committed rAFP8d98c4f533ee: New entry: Simple_Clause_Learning.

nipkow committed rAFPa054eadf858c: New entry Distributed_Distinct_Elements.

nipkow committed rAFPb6c8736b79bb: New entry No_FTL_observers_Gen_Rel.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP8c3574960b41: metadata for CommCSL + sitegen.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf323a37f60a5: added new files generated by sitegen.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd33f633d7f1f: new entry: CommCSL.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPc2b9a8deb55c: metadata for Expander Graphs.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP528b9fec7472: new entry: Expander Graphs.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP98e268419ce2: sitegen.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf30f86e45086: fix of toml-entries and rerun of sitegen: problem: links where in these quotes….

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPdb530be3d7ca: sitegen (for Binary_Code_Imprimitive and….

Fabian Huch <huch@in.tum.de> committed rAFPaa0bd4097a74: tuned;.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP25cfc0d55518: new entry: Binary_Code_Imprimitive.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP9490f09cf4e6: new entry: Two_Generated_Word_Monoids_Intersection.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP055662f88f96: metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb3d3356622c7: running sort on ROOTS.

nipkow committed rAFP2ad1cd4a0982: New entry Probability_Inequality_Completeness.

paulson committed rAFP5818f34777c7: Rensets metadata.

paulson <lp15@cam.ac.uk> committed rAFP838da7313b56: New entry Rensets.

nipkow committed rAFPcf0204d4e1a9: more Edwards.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP56f1ac262885: metadata and sitegen for CVP_Hardness.

nipkow committed rAFPc9533fbfcc4e: New entry Edwards_Elliptic_Curves_Group.

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP2c37a04d5c87: rerun sitegen.

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP33209b175741: revert proof compression experiment.

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP786b13f08c87: new entry: CVP_Hardness.

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP63f7ced67c2c: metadata for ABY3_Protocols.

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPbb04b4d77988: new entry ABY3_Protocols.

paulson <lp15@cam.ac.uk> committed rAFP3ba4d397d499: sitegen for Given_Clause_Loops.

paulson <lp15@cam.ac.uk> committed rAFP35cfa78f74c9: New entry Given_Clause_Loops.