- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
May 27 2021
May 27 2021
adapted to Isabelle/466fae6bf22e;
n.muendler <n.muendler@tum.de> committed rAFPe85ad91917fa: Remove comment about missing refinement.
Remove comment about missing refinement
paulson <lp15@cam.ac.uk> committed rAFP96fa84024913: continued uglification, but also fixed some dodgy proofs.
continued uglification, but also fixed some dodgy proofs
paulson <lp15@cam.ac.uk> committed rAFP0c01ef559f08: fixed some broken / looping / fragile proofs.
fixed some broken / looping / fragile proofs
sitegen for Padic_Ints
new entry: Padic_Ints
simplify usage instructions more
nipkow committed rAFP64cb55b26fa7: New entry: Regressioon_Test_Selection.
New entry: Regressioon_Test_Selection
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP073e8a114c2e: metadata for Metalogic_ProofChecker.
metadata for Metalogic_ProofChecker
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPa806650b5376: metadata for GaleStewart_Games.
metadata for GaleStewart_Games
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP8e9ea5fc7383: new entry Metalogic_ProofChecker.
new entry Metalogic_ProofChecker
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPb388d0d42d35: new entry GaleStewart_Games.
new entry GaleStewart_Games
paulson <lp15@cam.ac.uk> committed rAFP149d79fb9a89: new entry BenOr_Kozen_Reif.
new entry BenOr_Kozen_Reif
paulson <lp15@cam.ac.uk> committed rAFPc05cd976ec65: fixed the ROOT file ofr BenOr_Kozen_Reif.
fixed the ROOT file ofr BenOr_Kozen_Reif
paulson <lp15@cam.ac.uk> committed rAFPec17a4428a60: webpage for BenOr_Kozen_Reif.
webpage for BenOr_Kozen_Reif
paulson <lp15@cam.ac.uk> committed rAFPaf69398094b7: added a necessary acknowledgment (ERC).
added a necessary acknowledgment (ERC)
nipkow committed rAFP7cc207b26f4f: New entry Progress_Tracking.
New entry Progress_Tracking
paulson <lp15@cam.ac.uk> committed rAFP141f2e614ae3: Slight tidying to shorten too-long lines.
Slight tidying to shorten too-long lines
paulson <lp15@cam.ac.uk> committed rAFP7d686b4e8472: renamed a lemma.
renamed a lemma
paulson <lp15@cam.ac.uk> committed rAFPa3ee7515305a: Fixed an error in the statement of closed_subsets_empty. Also added syntax….
Fixed an error in the statement of closed_subsets_empty. Also added syntax…
paulson <lp15@cam.ac.uk> committed rAFP04ce41144de1: Revisions by Wenda to eliminate the locale comp_affine_scheme.
Revisions by Wenda to eliminate the locale comp_affine_scheme
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP7762d8091ebc: consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry +….
consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry +…
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP9a7c7db7a492: metadata for IFC_Tracking.
metadata for IFC_Tracking
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd6ecd2356690: new entry: Grothendieck_Schemes.
new entry: Grothendieck_Schemes
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP5b0b84d45ce8: new entry IFC_Tracking.
new entry IFC_Tracking
makarius committed rAFP5b4eeafc4c58: recover some patches after years of continuously changing Isabelle LaTeX output;.
recover some patches after years of continuously changing Isabelle LaTeX output;
prefer document_preprocessor over document_build;
adapted to Isabelle/ef1a18e20ace;
prefer document_logo instead of document_build script;
paulson <lp15@cam.ac.uk> committed rAFPe28d0bec47d2: PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of….
PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of…
paulson <lp15@cam.ac.uk> committed rAFPfc32ad9925ee: fixed two more "sorted" errors.
fixed two more "sorted" errors
paulson <lp15@cam.ac.uk> committed rAFPfdbe2f5933e8: fixed two "sorted" issues.
fixed two "sorted" issues
paulson <lp15@cam.ac.uk> committed rAFP02b3a52be010: changes for "sorted" as an abbreviation.
changes for "sorted" as an abbreviation
May 26 2021
May 26 2021
more robust syntax;
clarified document export names;
makarius committed rISABELLE466fae6bf22e: compose Latex text as XML, output exported YXML in Isabelle/Scala;.
compose Latex text as XML, output exported YXML in Isabelle/Scala;
makarius committed rISABELLE0909fd14f8a4: avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;.
avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;
makarius committed rISABELLE546e1e591635: more direct index_entry: no positions required -- text is eventually moved to ..
more direct index_entry: no positions required -- text is eventually moved to .
clarified signature;
May 25 2021
May 25 2021
dcjm committed rPOLYML2b78b6865011: Enable all signals in child process after Unix.execute/executeInEnv. (authored by dcjm).
Enable all signals in child process after Unix.execute/executeInEnv.
dcjm committed rPOLYML00a5653c7373: The file part of the command for Unix.execute/executeInEnv should be included… (authored by dcjm).
The file part of the command for Unix.execute/executeInEnv should be included…
May 24 2021
May 24 2021
dcjm committed rPOLYML8185978a586a: Enable all signals in child process after Unix.execute/executeInEnv. (authored by dcjm).
Enable all signals in child process after Unix.execute/executeInEnv.
makarius committed rISABELLE52e43a93d51f: clarified system_log: make this work independently of the particular "isabelle….
clarified system_log: make this work independently of the particular "isabelle…
proper signature export (amending b50f8cc8c08e);
tuned message, e.g. for Pure bootstrap;
syslog option for "isabelle build";
May 23 2021
May 23 2021
makarius committed rISABELLEac7f41b66e1b: further "unset CDPATH", whenever a new non-interactive bash is started (see….
further "unset CDPATH", whenever a new non-interactive bash is started (see…
clarified index, more like formal @{element_ref};
clarified treatment of type constructors;
misc tuning and clarification;
makarius committed rISABELLEebaed09ce06e: more uniform document antiquotations for ML: consolidate former setup for….
more uniform document antiquotations for ML: consolidate former setup for…
makarius committed rISABELLEeccc4a13216d: clarified index antiquotation for ML: more ambitious type-setting, more….
clarified index antiquotation for ML: more ambitious type-setting, more…
clarified, e.g. type variables;
clarified signature: avoid dispatch via name;
more ambitious default for index "is like";
support for index entries;
clarified old document build;
makarius committed rISABELLE8c460c09665e: prefer standard document_build=lualatex --- no impact of "sedindex" in….
prefer standard document_build=lualatex --- no impact of "sedindex" in…
makarius committed rISABELLEe78c8a1f03fb: prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been….
prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been…
makarius committed rISABELLEbeeebae99746: prefer explicit option document_bibliography (actually ignored by build script);.
prefer explicit option document_bibliography (actually ignored by build script);
explicit option document_bibliography;
proper bibliography;
discontinued obsolete "isabelle latex";
makarius committed rISABELLEc46ff0efa1ce: more direct use of latex tools: avoid diversion into "isabelle latex -o pdf"….
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf"…
default document_build (lualatex);
makarius committed rISABELLE6638323d2774: clarified bash scripts, with public interfaces for user-defined Document_Build..
clarified bash scripts, with public interfaces for user-defined Document_Build.
more robust: allow \printindex within the document;
option document_preprocessor;
show symbols in Isabelle/ML instead of perl;
makarius committed rISABELLEb13b2c1d419e: more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using….
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using…
tuned --- more robust;
makarius committed rISABELLEa1ef2589c33f: discontinued somewhat pointless "fixbookmarks": default output works….
discontinued somewhat pointless "fixbookmarks": default output works…
makarius committed rISABELLE2f023b2b0e1e: more uniform bibtex error, without using perl (see 4710dd5093a3);.
more uniform bibtex error, without using perl (see 4710dd5093a3);