- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Mar 27 2021
Mar 27 2021
more robust invocation of hg;
more robust: idempotent;
more robust invocation of hg;
more robust invocation of hg;
makarius committed rISABELLE0e880b793db1: support repository archives (without full .hg directory);.
support repository archives (without full .hg directory);
makarius committed rISABELLE1be70e3de751: record official releases that follow a certain structure, with public access….
record official releases that follow a certain structure, with public access…
Mar 25 2021
Mar 25 2021
Update tile to match metadata
Extend entry Szpilrajn
dedicated session for combinatorial material
dedicated session for combinatorial material
Mar 24 2021
Mar 24 2021
makarius committed rISABELLE6b480efe1bc3: support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;.
support for Java Chromium Embedded Framework (JCEF): still somewhat fragile;
Mar 23 2021
Mar 23 2021
enforce full build;
makarius committed rISABELLE4e12a6caefb3: turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;.
turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont;
makarius committed rISABELLE2cc9bd9a7357: discontinue fragile check in LaTeX, e.g. problems with toc entries;.
discontinue fragile check in LaTeX, e.g. problems with toc entries;
Mar 22 2021
Mar 22 2021
paulson <lp15@cam.ac.uk> committed rISABELLE76095cffcc2b: type class relaxation.
type class relaxation
clarified group (but hard to tell);
makarius committed rISABELLE090add96f5f9: more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb….
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb…
makarius committed rISABELLE1e5c1f8a35cd: clarified package name (actually both pxfonts and txfonts exist and have this….
clarified package name (actually both pxfonts and txfonts exist and have this…
Mar 21 2021
Mar 21 2021
prefer isabelle bbbfont;
enforce full build;
clarified symbol names, notably relevant for Z_Notation;
makarius committed rISABELLE1f1f4462a6ae: high-quality blackboard-bold fonts from "txmia" (package "txfonts");.
high-quality blackboard-bold fonts from "txmia" (package "txfonts");
update README (actually after update of component);
Mar 19 2021
Mar 19 2021
publish component;
makarius committed rISABELLE3ede182a479a: further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F….
further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F…
clarified \<Zcomp> (small) vs. \<Zsemi> (big);
more Z_Notation symbols, as proposed by Simon Foster;
Mar 18 2021
Mar 18 2021
makarius committed rISABELLE519ce76a602f: more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the….
more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the…
clarified order for GUI panel;
prefer more direct interpretation
more Z_Notation symbols, as proposed by Simon Foster;
makarius committed rISABELLE7ca886bf7156: more accurate spacing, according to results seen in isar-ref (Appendix B)….
more accurate spacing, according to results seen in isar-ref (Appendix B)…
makarius committed rISABELLE76a061b67993: clarified order for presentation in isar-ref (Appendix B);.
clarified order for presentation in isar-ref (Appendix B);
makarius committed rISABELLE2200a19cac72: prefer explicit \<Zproject> (with its own Unicode codepoint);.
prefer explicit \<Zproject> (with its own Unicode codepoint);
Mar 17 2021
Mar 17 2021
makarius committed rISABELLEd1c4c2395650: more Isabelle symbol definitions for Z Notation, based on https://github..
more Isabelle symbol definitions for Z Notation, based on https://github.
proper directory of settings file;
Basically currently the proof format of Z3 has bugs that we cannot solve on the Isabelle side (https://github.com/Z3Prover/z3/issues/5073). Fixing those requires either internal Z3 knowledge or time from a Z3 developer.
Mar 16 2021
Mar 16 2021
paulson <lp15@cam.ac.uk> committed rAFPdf8dbc70db27: Removal of an unused theorem. Plus lots of white space.
Removal of an unused theorem. Plus lots of white space
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP9cf49cbf016c: switch new entries' documents to T1 encoding.
switch new entries' documents to T1 encoding
Mar 15 2021
Mar 15 2021
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP87af554341ac: merge from afp-2021.
merge from afp-2021
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP0bcae60315c9: sitegen for Modular_arithmetic_LLL_and_HNF_algorithms.
sitegen for Modular_arithmetic_LLL_and_HNF_algorithms
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP83eb79b52c4d: corrected metadata (use acute's in names of J. Divasón and René T.).
corrected metadata (use acute's in names of J. Divasón and René T.)
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP137c96131780: metadata for Modular_arithmetic_LLL_and_HNF_algorithms.
metadata for Modular_arithmetic_LLL_and_HNF_algorithms
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP05123cb597d8: new entry Modular_arithmetic_LLL_and_HNF_algorithms.
new entry Modular_arithmetic_LLL_and_HNF_algorithms
paulson <lp15@cam.ac.uk> committed rAFP3a75cadaa25e: a slight streamlining.
a slight streamlining
paulson <lp15@cam.ac.uk> committed rAFP6ada28be8b27: Hermite_Lindemann website.
Hermite_Lindemann website
paulson <lp15@cam.ac.uk> committed rAFPa9fb9e1730a7: new entry Hermite_Lindemann.
new entry Hermite_Lindemann
paulson <lp15@cam.ac.uk> committed rAFP39b6774669ae: cosmetic changes.
cosmetic changes
paulson <lp15@cam.ac.uk> committed rAFP6f59082548d0: Projective_Measurements with files.
Projective_Measurements with files
paulson <lp15@cam.ac.uk> committed rAFP27f38e928e7b: Projective_Measurements website.
Projective_Measurements website
add Andreas Lochbihler as editor
paulson <lp15@cam.ac.uk> committed rAFP4cee739acb88: new entry Projective_Measurements.
new entry Projective_Measurements
tuned signature (again);
desharna committed rAFPfce965a689cd: refactored and added lemma state_behaves_forward_to_backward.
refactored and added lemma state_behaves_forward_to_backward
dcjm committed rPOLYML1d8e4c644a70: Don't block signals if we run with --singlethread. (authored by dcjm).
Don't block signals if we run with --singlethread.
dcjm committed rPOLYMLbab587394374: Add an option to disable thread creation and run everything on a single thread. (authored by dcjm).
Add an option to disable thread creation and run everything on a single thread.
Mar 14 2021
Mar 14 2021
tuned --- following hints by IntelliJ;
proper shell quote;
removed spurious references to perl / libwww-perl;
makarius committed rISABELLE1cc848548f21: invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without….
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without…
makarius committed rISABELLE00b77365552e: clarified signature: refer to file name instead of file content;.
clarified signature: refer to file name instead of file content;
clarified signature: more explicit types;
makarius committed rISABELLEf27d7b12e8a4: support for SystemOnTPTP.run_system, with strict error following….
support for SystemOnTPTP.run_system, with strict error following…
makarius committed rISABELLE8970081c6500: elapsed time to download content (and for the server to provide content);.
elapsed time to download content (and for the server to provide content);
clarified signature;
Mar 13 2021
Mar 13 2021
makarius committed rISABELLE9d1b5c0bdec8: more direct elapsed run_time via bash_process wrapper (via Scala and C);.
more direct elapsed run_time via bash_process wrapper (via Scala and C);
makarius committed rISABELLEbd8bce50b9d4: use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and….
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and…
makarius committed rISABELLE2b657a70116c: clarified signature: url may change dynamically and is part of result;.
clarified signature: url may change dynamically and is part of result;
makarius committed rISABELLEd0f529d5c5c9: clarified signature: let Sledgehammer handle SystemOnTPTP comments;.
clarified signature: let Sledgehammer handle SystemOnTPTP comments;
clarified signature;
support timeout, similar to perl LWP::UserAgent;
makarius committed rISABELLE7d7d959547a1: support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);.
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
makarius committed rISABELLE22f3f2117ed7: clarified signature: function_thread is determined in Isabelle/Scala, not….
clarified signature: function_thread is determined in Isabelle/Scala, not…
clarified HTTP.Content: support encoding;
clarified signature: more explicit HTTP operations;