Tidied several ugly proofs in some elderly examples — paulson <lp15@cam.ac.uk> / hgweb
tuned message; — wenzelm / hgweb
clarified errors; — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
support Node.js as well, reusing the engine from Electron/VSCodium; — wenzelm / hgweb
updated to vscode 1.65.2; — wenzelm / hgweb
proper result check; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified directory layout and settings: more robust on all platforms; — wenzelm / hgweb
tuned; — wenzelm / hgweb
support Electron application framework;
clarified vscodium startup; — wenzelm / hgweb
generated lemma map_ident_strong for BNFs — desharna / hgweb
updated SMT certificates — desharna / hgweb
used more descriptive assert names in SMT-Lib output — desharna / hgweb

#95 (Mar 13, 2022, 12:14:00 AM)

clarified and unified executable names; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — wenzelm / hgweb
suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode; — wenzelm / hgweb
fix handling of lambdas in reconstruction of eq_congruent — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
more robust: avoid breakdown of Search dialog; — wenzelm / hgweb
tuned; — wenzelm / hgweb
always use Isabelle encoding, as in Isabelle/jEdit; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature: more uniform ts vs. Scala; — wenzelm / hgweb
discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
discontinued special treatment of workspace_dir as session directory; — wenzelm / hgweb
actually decode/encode symbols; — wenzelm / hgweb
merged — wenzelm / hgweb
prefer yarn over npm; — wenzelm / hgweb
more accurate .hgignore; — wenzelm / hgweb
clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode; — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
proper init_resources for macos; — wenzelm / hgweb
clarified names; — wenzelm / hgweb
clarified modules: vscode vs. extension;
clarified signature; — wenzelm / hgweb
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs; — wenzelm / hgweb
more operations; — wenzelm / hgweb
tuned comments;
tuned messages; — wenzelm / hgweb
patch VSCode source tree to support isabelle_encoding.ts; — wenzelm / hgweb
more robust, pass "yarn valid-layers-check"; — wenzelm / hgweb
clarified directories; — wenzelm / hgweb
patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet; — wenzelm / hgweb
fit into vscode source conventions; — wenzelm / hgweb
A tiny further cleanup — paulson <lp15@cam.ac.uk> / hgweb
Tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — nipkow / hgweb
more count_list lemmas — nipkow / hgweb
towards UTF-8-Isabelle symbol encoding; — wenzelm / hgweb
updated to VSCode 1.65.0; — wenzelm / hgweb
clarified char symbols: cover most European languages; — wenzelm / hgweb
more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML); — wenzelm / hgweb
tuned comments;
tuned imports; — wenzelm / hgweb
more robust dependencies: avoid implicit update, escpecially of underlying vscode engine; — wenzelm / hgweb
proper file headers; — wenzelm / hgweb
added count_list lemmas — nipkow / hgweb
tuned message; — wenzelm / hgweb
more compact result; — wenzelm / hgweb
prepare patched version more thoroughly, with explicit patches; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb

#95 (Mar 13, 2022, 12:14:00 AM)

more count_list lemmas — nipkow / hgweb
more count_list — nipkow / hgweb
merged — nipkow / hgweb
moved some count_list lemmas — nipkow / hgweb
synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
continue 98838b260ed4 — Frédéric Tuong / hgweb
continue ee01bce2ecca — Frédéric Tuong / hgweb
cancel some part of 11d4567f1b99 — Frédéric Tuong / hgweb
cancel some part of 98838b260ed4 — Frédéric Tuong / hgweb
cancel some part of ada85c62541d — Frédéric Tuong / hgweb
synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb

#94 (Mar 6, 2022, 12:14:00 AM)

recover platform-specific node binaries from original download, notably for node-pty for Terminal; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned imports; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
more executable files;
clarified modules; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned output; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified command-line options; — wenzelm / hgweb
update official Isabelle release, notably for "Admin/init -R"; — wenzelm / hgweb
more robust; — wenzelm / hgweb
build component for VSCodium (cross-compiled from sources for all platforms); — wenzelm / hgweb
tuned signature: more robust operation; — wenzelm / hgweb
clarified order; — wenzelm / hgweb
proper antiquotations (amending ff784d5a5bfb); — wenzelm / hgweb
clarified signature: file operations take standard_path as in Isabelle/ML/Scala; — wenzelm / hgweb
provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol; — wenzelm / hgweb
proper init of non-existing file; — wenzelm / hgweb
proper function call; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5); — wenzelm / hgweb
misc tuning, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature;
clarified data structures; — wenzelm / hgweb
tuned imports; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
misc tuning, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
support for file-system operations; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
follow standard Isabelle license --- no longer published on market place; — wenzelm / hgweb
tuned README; — wenzelm / hgweb
disregard public marketplace; — wenzelm / hgweb
tuned imports; — wenzelm / hgweb
more robust; — wenzelm / hgweb
merged — wenzelm / hgweb
tuned message; — wenzelm / hgweb
clarified module; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
added documentation for new VSCode modules; — Fabian Huch <huch@in.tum.de> / hgweb
proper monospace font for terminal; — wenzelm / hgweb
merged — wenzelm / hgweb
tuned; — wenzelm / hgweb
support system path representations (as in Isabelle/Java/Scala); — wenzelm / hgweb
auto-update; — wenzelm / hgweb
more robust; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified rendering; — wenzelm / hgweb
prefer hardwired locale; — wenzelm / hgweb
more aggressive activation; — wenzelm / hgweb
Added some theorems (from Wetzel) — paulson <lp15@cam.ac.uk> / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
disable extension updates; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
disable check for updates: support just one static version; — wenzelm / hgweb
misc tuning based on comments by Heiko Eißfeldt; — wenzelm / hgweb
misc tuning based on comments by Heiko Eißfeldt; — wenzelm / hgweb

#94 (Mar 6, 2022, 12:14:00 AM)

split locale in two — desharna / hgweb
Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
added some alternative proofs in Smith_Normal_Form entry — jodivaso / hgweb
The last tranche of material to be moved to the complex analysis libraries — paulson <lp15@cam.ac.uk> / hgweb
Removal of material that has since been added to ZFC_in_HOL.General_Cardinals — paulson <lp15@cam.ac.uk> / hgweb

#93 (Feb 27, 2022, 12:14:00 AM)

removed junk; — wenzelm / hgweb
some updates to README.md; — wenzelm / hgweb
clarified default settings; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
support Isabelle fonts via patch of vscode resources; — wenzelm / hgweb
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249); — wenzelm / hgweb
clarified symbolic path; — wenzelm / hgweb
clarified extension name (again); — wenzelm / hgweb
removed obsolete material; — wenzelm / hgweb
update scripts, based on recent "yo code" template; — wenzelm / hgweb
clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.); — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified extension name; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified options; — wenzelm / hgweb
support local .vsix installation;
discontinued publishing to VSCode Marketplace, which will become obsolete eventually; — wenzelm / hgweb
formal record of generated package-lock.json; — wenzelm / hgweb
pro-forma update of version, for ongoing development; — wenzelm / hgweb
updated notes on Isabelle/VSCode development; — wenzelm / hgweb
proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode; — wenzelm / hgweb
simp rules for negative numerals — haftmann / hgweb
updated vscode extension: proper recoding; — Fabian Huch <huch@in.tum.de> / hgweb
tuned vscode extension; — Fabian Huch <huch@in.tum.de> / hgweb
tuned vscode extension: split isabelle fsp into workspace and mapping; — Fabian Huch <huch@in.tum.de> / hgweb
update VSCode plugin dependencies; — Fabian Huch <huch@in.tum.de> / hgweb
added Isabelle output panel to VSCode extension; — Fabian Huch <huch@in.tum.de> / hgweb
Simplified a couple of extremely long and ugly apply-proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — wenzelm / hgweb
some updates to README.md; — wenzelm / hgweb
refer to Isabelle settings via environment, which is provided via "isabelle vscode";
clarified error handling; — wenzelm / hgweb
more operations; — wenzelm / hgweb
more robust startup wrt. VSCode workspace (by Fabian Huch); — wenzelm / hgweb
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch); — wenzelm / hgweb
have Sledgehammer honor 'smt_nat_as_int' option — blanchet / hgweb
more handling of Zipperposition definitions in Isar proof construction — blanchet / hgweb
handle Zipperposition definitions in Isar proof construction — blanchet / hgweb
parse Zipperposition definitions — blanchet / hgweb
clarified URL; — wenzelm / hgweb
clarified pdf path; — wenzelm / hgweb
HTTP view of Isabelle PDF documentation; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
more robust; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
clarified signature: more explicit section structure; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified URL (again); — wenzelm / hgweb
more robust toplevel url: allow extra "/"; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature;
clarified URLs; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
support for PDF.js: platform-independent PDF viewer; — wenzelm / hgweb
more robust mime_type; — wenzelm / hgweb
merged — wenzelm / hgweb
improved support for Java Chromium Embedded Framework (JCEF): works on x86_64-linux and x86_64-windows with jdk-15 (not jdk-17), does not work on arm64 and darwin; — wenzelm / hgweb
one new lemma — paulson <lp15@cam.ac.uk> / hgweb
clarified options; — wenzelm / hgweb
clarified options; — wenzelm / hgweb
clarified directory; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
prefer strict equality, without implicit type conversion; — wenzelm / hgweb
tuned; — wenzelm / hgweb
auto-update by VSCode; — wenzelm / hgweb
more activationEvents, as proposed by Denis Paluca; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
run Isabelle/VSCode using local VSCodium installation; — wenzelm / hgweb
provide macos_exe, based on bin/codium from linux; — wenzelm / hgweb
clarified options; — wenzelm / hgweb
Avoid overaggresive splitting. — haftmann / hgweb
more lemmas for distribution — haftmann / hgweb
Avoid overaggresive simplification. — haftmann / hgweb
merged — wenzelm / hgweb
setup VSCode from VSCodium distribution; — wenzelm / hgweb
more robust package_dir, to increase chances that it works with IntelliJ IDEA; — wenzelm / hgweb
NEWS — desharna / hgweb
Mirabelle now considers goals preceding "unfolding" and "using" commands — desharna / hgweb

#93 (Feb 27, 2022, 12:14:00 AM)

Deleted nearly 200 lines of unused material — paulson <lp15@cam.ac.uk> / hgweb
A new theorem — paulson <lp15@cam.ac.uk> / hgweb
Clarified code module names. — haftmann / hgweb
removed ancient numeral representation — haftmann / hgweb
restore state of VYDRA_MDL to b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
metadata for Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
New entry Wetzel's Problem — nipkow / hgweb
metadata for Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
metadata for VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
Backed out changeset c9f94b0ae10e — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Backed out changeset b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
metadata update for VYDRA_MDL — mraszyk / hgweb
New entry: VYDRA_MDL — mraszyk / hgweb
fixed failing proofs — desharna / hgweb
New definition of the Aleph operator so that it's defined for all arguments, not just ordinals — paulson <lp15@cam.ac.uk> / hgweb
ALEXANDRIA acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
New set theory lemmas about cardinality (mainly) — paulson <lp15@cam.ac.uk> / hgweb
Another attempt for a consolidated terminology. — haftmann / hgweb
Avoid overaggresive splitting. — haftmann / hgweb
more lemmas for distribution — haftmann / hgweb
Avoid overaggresive simplification. — haftmann / hgweb
some new lemmas — paulson <lp15@cam.ac.uk> / hgweb

#92 (Feb 20, 2022, 12:14:00 AM)

merged — paulson / hgweb
an assortment of new or stronger lemmas — paulson <lp15@cam.ac.uk> / hgweb
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented; — wenzelm / hgweb
print outcome of Sledgehammer search in panel — blanchet / hgweb
print Sledgehammer error message — blanchet / hgweb

#92 (Feb 20, 2022, 12:14:00 AM)

merged — nipkow / hgweb
More material — nipkow / hgweb
added idempotent most general unifier — desharna / hgweb
used same parameter order for locales substitution and substitution — desharna / hgweb
patched for new/simplified lemmas — paulson <lp15@cam.ac.uk> / hgweb
Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb

#91 (Feb 13, 2022, 12:14:00 AM)

updated documentation to current matter of affairs — haftmann / hgweb
unused; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
merged — desharna / hgweb
added Isabelle identification to Mirabelle output — desharna / hgweb
uniformized fact selection for ATP and SMT in Sledgehammer — desharna / hgweb
provide cache for slow computations; — wenzelm / hgweb
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer — desharna / hgweb
more operations; — wenzelm / hgweb
more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson) — blanchet / hgweb
more robust TSTP proof parsing — blanchet / hgweb
added possibility of extra options to SMT slices — blanchet / hgweb

#91 (Feb 13, 2022, 12:14:00 AM)

merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
avoid conflict with index.html in generated html — Gerwin Klein <kleing@unsw.edu.au> / hgweb
New entry: FO_Theory_Rewriting — nipkow / hgweb
Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency.

+ Remove obsolete e-mail from notification mailing list. — Emin Karayel <me@eminkarayel.de> / hgweb
Improve proofs for Interpolation_Polynomials_HOL_Algebra.

Reduced the number of apply scripts used. — Emin Karayel <me@eminkarayel.de> / hgweb
Correct date. — Asta Halkjær From <andro.from@gmail.com> / hgweb
deleted a lemma that's in the devel library — paulson <lp15@cam.ac.uk> / hgweb
Cleanup and new results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
moved theorems into Matrix.thy — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
merge of AFP 2021-1 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
New AFP entry: Equivalence_Relation_Enumeration — nipkow / hgweb
new entry: LP_Duality — nipkow / hgweb
cosmetic tweaks — paulson <lp15@cam.ac.uk> / hgweb
sitegen and metadata for Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
metadata for Quasi_Borel_Spaces, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Quasi_Borel_Spaces — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sitegen for FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
new entry FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
tweak: corollary that the ln also yields irrational numbers — paulson <lp15@cam.ac.uk> / hgweb
New entry: Interpolation_Polynomials_HOL_Algebra — nipkow / hgweb
Finally remembered to run sitegen — paulson <lp15@cam.ac.uk> / hgweb
Fixed the meta data in the abstract as well — paulson <lp15@cam.ac.uk> / hgweb
Eliminated the references to SOS (which is no longer used) and changed to the document style to "article". — paulson <lp15@cam.ac.uk> / hgweb
typo — nipkow / hgweb
typo — nipkow / hgweb
New entry Irrationals_From_THEBOOK — nipkow / hgweb
new entry Median_Method — nipkow / hgweb
Actuarial Mathematics website — paulson <lp15@cam.ac.uk> / hgweb
New entry Actuarial_Mathematics — paulson <lp15@cam.ac.uk> / hgweb

#90 (Feb 6, 2022, 12:14:00 AM)

tuned output syntax: Hoare triples are now blocks — nipkow / hgweb
tuned output syntax: INV and VAR are now blocks — nipkow / hgweb
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)') — blanchet / hgweb
enable induction in one of Zipperposition's slices — blanchet / hgweb
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme — blanchet / hgweb
robustly handle empty proof blocks in Isar proof output — blanchet / hgweb
propagate right result when enough proofs have been found — blanchet / hgweb
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives — blanchet / hgweb
don't lose error messages — blanchet / hgweb
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice — blanchet / hgweb
careful with partial applications — blanchet / hgweb
don't perform preplaying steps if preplaying is disabled — blanchet / hgweb
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs — blanchet / hgweb
tuned punctuation — blanchet / hgweb
handle TPTP '!=' more gracefully in Isar proof reconstruction — blanchet / hgweb
guard against duplicate lines in Zipperposition proofs — blanchet / hgweb
tuning — blanchet / hgweb
tuned NEWS — blanchet / hgweb
compile HOL-TPTP — blanchet / hgweb
compile Metis_Examples — blanchet / hgweb
more NEWS — blanchet / hgweb
compile mirabelle — blanchet / hgweb
tweaked Auto Sledgehammer's behavior and output — blanchet / hgweb
updated NEWS — blanchet / hgweb
removed experimental prover z3_tptp — blanchet / hgweb
print more verbose information — blanchet / hgweb
run all installed provers by default — blanchet / hgweb
update slice options centrally — blanchet / hgweb
further work on new Sledgehammer slicing — blanchet / hgweb
tweaked verbose output — blanchet / hgweb
tweak padding of prover slice schedule to include all provers — blanchet / hgweb
implemented 'max_proofs' mechanism — blanchet / hgweb
document new option 'max_proofs' — blanchet / hgweb
crude implementation of centralized slicing — blanchet / hgweb
removed obscure E option — blanchet / hgweb
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set — blanchet / hgweb
rationalize slicing format — blanchet / hgweb
thread slices through — blanchet / hgweb
simplified 'best_slice' data structure and made minor changes to slices — blanchet / hgweb
changed logic of 'slice' option to 'slices' — blanchet / hgweb
updated documentation of 'slice' (now 'slices') option — blanchet / hgweb
revised Sledgehammer documentation — blanchet / hgweb
rationalized output for forthcoming slicing model — blanchet / hgweb
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code — blanchet / hgweb
disable slicing within ATP module (in preparation for refactoring) — blanchet / hgweb
disable slicing within SMT (in preparation for factoring it out) — blanchet / hgweb
generalized the 'slice' option towards more flexible slicing — blanchet / hgweb
tuned -- fewer warnings; — wenzelm / hgweb

#90 (Feb 6, 2022, 12:14:00 AM)

Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Fix LaTeX issue. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Qualification required(?) — nipkow / hgweb
merged — nipkow / hgweb
more variants of the algorithm — nipkow / hgweb
Added funding acknowledgments.
Fixed broken BibTeX citation. — Dominique Unruh <unruh@ut.ee> / hgweb
Strong completeness for PAL systems. — Asta Halkjær From <andro.from@gmail.com> / hgweb

#89 (Jan 30, 2022, 12:14:00 AM)

Added a tiny proof — paulson <lp15@cam.ac.uk> / hgweb
Deletion of a duplicate proof — paulson <lp15@cam.ac.uk> / hgweb
useful lemma integral_less — paulson <lp15@cam.ac.uk> / hgweb
merged — desharna / hgweb
removed unused parameter following f9908452b282 — desharna / hgweb
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis) — blanchet / hgweb
fixed dodgy intro! attributes — paulson <lp15@cam.ac.uk> / hgweb
merged — desharna / hgweb
optimized facts traversal in TPTP translation — desharna / hgweb
optimized app_op_level selection in TPTP generation — desharna / hgweb
tuned trivial check in mirabelle_sledgehammer — desharna / hgweb
renamed run_action to run in Mirabelle.action record — desharna / hgweb
added spying of fact filtering timing — desharna / hgweb
tuned mirabelle_sledgehammer output — desharna / hgweb
added spying to Sledgehammer — desharna / hgweb
proper fact filter for dummy ATPs — desharna / hgweb
added syping of fact filtering time to sledgehammer — desharna / hgweb
removed unsynchronized references in mirabelle_sledgehammer — desharna / hgweb
tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run — desharna / hgweb
updated to polyml-test-15c840d48c9a; — wenzelm / hgweb

#89 (Jan 30, 2022, 12:14:00 AM)

Cleanup. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Fewer parentheses around turnstile + remove unused lemmas. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Simplify proof of truth lemma. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Notation for `imply` and fewer parenthesis around turnstiles. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Abstract results to shorten proofs. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
merged — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
more symbols; — wenzelm / hgweb
profer bundle lattice_syntax; — wenzelm / hgweb
prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended; — wenzelm / hgweb
Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5. — Asta Halkjær From <andro.from@gmail.com> / hgweb
avoid hardwired document output; — wenzelm / hgweb
merged — paulson / hgweb
deleting the overloading of div and mod, with its attendant ambiguities — paulson <lp15@cam.ac.uk> / hgweb
replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb

#88 (Jan 23, 2022, 12:14:00 AM)

some updates and clarification on Assumption.export_term; — wenzelm / hgweb
new theorem has_integral_UN — paulson <lp15@cam.ac.uk> / hgweb
updated to jdk-17.0.2+8; — wenzelm / hgweb
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads — desharna / hgweb
NEWS — desharna / hgweb
added Mirabelle option "-y" for dry run — desharna / hgweb
tuned garbage optimization — desharna / hgweb
added cpu time (in ms) to Mirabelle run_action output — desharna / hgweb
added Mirabelle option -r to randomize the goals before selection — desharna / hgweb
A new lemma about inverse image — paulson <lp15@cam.ac.uk> / hgweb
proper treatment of $let variables in symbol table in Sledgehammer — desharna / hgweb
removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer — desharna / hgweb

#88 (Jan 23, 2022, 12:14:00 AM)

Removal of a lemma (now in the libraries) and a few tweaks — paulson <lp15@cam.ac.uk> / hgweb

#87 (Jan 16, 2022, 12:14:00 AM)

merged — desharna / hgweb
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir" — desharna / hgweb
proper name mangling of "undefined" constants in Sledgehammer — desharna / hgweb
earlier availability of lifting — haftmann / hgweb
more correct transfer — haftmann / hgweb
merged — desharna / hgweb
proper abstraction of function variables when instantiating induction rules in Sledgehammer — desharna / hgweb
added lemma asympD — desharna / hgweb
added lemma — nipkow / hgweb
Some lemmas about continuous functions with integral zero — paulson <lp15@cam.ac.uk> / hgweb

#87 (Jan 16, 2022, 12:14:00 AM)

Tuning. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
merged — paulson / hgweb
tweaks — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
Fixed an inadequate description — paulson <lp15@cam.ac.uk> / hgweb
tuned — haftmann / hgweb
mv to distribution — nipkow / hgweb
by now in distribution — nipkow / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
fixed abstract — nipkow / hgweb
tuned — nipkow / hgweb
website and metadata for Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sorted ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
tuned — nipkow / hgweb
New entry Knights_Tour — nipkow / hgweb
more thoroughly replace Michael Foster's e-mail address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
metadata and sitegen for Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
update Michael Forster's email address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
metadata and sitegen for Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
typo — nipkow / hgweb
merged — nipkow / hgweb
New entry Regular_Tree_Relations — nipkow / hgweb
We DON'T want an output directory — paulson <lp15@cam.ac.uk> / hgweb
MDP-Algorithms website — paulson <lp15@cam.ac.uk> / hgweb
new entry MDP-Algorithms — paulson <lp15@cam.ac.uk> / hgweb
typo — paulson <lp15@cam.ac.uk> / hgweb
new entry MDP-Rewards — paulson <lp15@cam.ac.uk> / hgweb
fixed typo — paulson <lp15@cam.ac.uk> / hgweb

#86 (Jan 9, 2022, 12:14:00 AM)

merged — desharna / hgweb
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp — desharna / hgweb
removed $ite from E 2.6 in THF format — desharna / hgweb
New and simplified theorems — paulson <lp15@cam.ac.uk> / hgweb
merged — desharna / hgweb
prefixed all mirabelle_sledgehammer output lines with sledgehammer output — desharna / hgweb

#86 (Jan 9, 2022, 12:14:00 AM)

CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
used wfP_imp_asymp from HOL — desharna / hgweb
simplified proof some more — desharna / hgweb
simplified proof — desharna / hgweb
Extended protocol model to support composition of more than two protocols without
the need of re-labeling them, additional automated checks, tighter integration
of the stateful protocol model and the automated verification (PSPSP) tool. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb

#85 (Jan 2, 2022, 12:14:00 AM)

added lemma — nipkow / hgweb
Tiny additions inspired by Roth development — paulson <lp15@cam.ac.uk> / hgweb

#85 (Jan 2, 2022, 12:14:00 AM)

Tweaked some failing proofs — paulson <lp15@cam.ac.uk> / hgweb

#84 (Dec 26, 2021, 12:14:00 AM)

allow general command transactions with presentation; — wenzelm / hgweb
more operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
support Gradle as alternative to Maven (again); — wenzelm / hgweb
tuned mirabelle command-line help message — desharna / hgweb
updated Mirabelle documentation — desharna / hgweb
proper documentation for induction_rules Sledgehammer option — desharna / hgweb
NEWS — desharna / hgweb
merged — desharna / hgweb
used TH1 for Leo-III in sledgehammer — desharna / hgweb
tuned run_sledgehammer and called it directly from Mirabelle — desharna / hgweb
exported Sledgehammer.launch_prover and use it in Mirabelle — desharna / hgweb
proper filtering inf induction rules in Mirabelle — desharna / hgweb
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle — desharna / hgweb
tuned ATP to use is_widely_irrelevant_const — desharna / hgweb
added support for initialization messages to Mirabelle — desharna / hgweb

#84 (Dec 26, 2021, 12:14:00 AM)

adapted to new Sledgehammer.run_sledgehammer return type — desharna / hgweb

#83 (Dec 19, 2021, 12:14:00 AM)

tuned comment — blanchet / hgweb
support for JSON:API; — wenzelm / hgweb
support for Flarum server; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
tuned imports; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
clarified author names; — wenzelm / hgweb
clarified author names; — wenzelm / hgweb
merged — wenzelm / hgweb
more accurate names;
complete coverage of mail addresses; — wenzelm / hgweb
more standard author_info; — wenzelm / hgweb
clarified author info and cluster nodes; — wenzelm / hgweb
more data integrity: name vs. address; — wenzelm / hgweb
clarified signature: more operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more data integrity: name vs. address; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
merged — desharna / hgweb
tuned ATP to use fold_index — desharna / hgweb
tuned sledgehammer to use map_index — desharna / hgweb
merged — wenzelm / hgweb
more data integrity: name vs. address; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
clarified name; — wenzelm / hgweb
more mailing list content; — wenzelm / hgweb
more mailing list content; — wenzelm / hgweb
updated links; — wenzelm / hgweb
added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff; — wenzelm / hgweb
tuned ATP to use map_index — desharna / hgweb
removed obsolete RC tags; — wenzelm / hgweb
proper path; — wenzelm / hgweb
merged, resolving conflict in src/Doc/Implementation/Logic.thy; — wenzelm / hgweb
Added tag Isabelle2021-1 for changeset c2a2be496f35 — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper ML types (amending 1aa92bc4d356); — wenzelm / hgweb
proper types for Scala.Fun instances (amending 1aa92bc4d356); — wenzelm / hgweb
proper syntax category; — wenzelm / hgweb

#83 (Dec 19, 2021, 12:14:00 AM)

Strengthened a lemma — paulson <lp15@cam.ac.uk> / hgweb
updated the definition of scheme — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
add change history — Gerwin Klein <kleing@unsw.edu.au> / hgweb
updated 2021-1 release dates -> web — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
ignore generated files — Gerwin Klein <kleing@unsw.edu.au> / hgweb
add 2021-1 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
set devel version again — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Added tag Isabelle2021-1 for changeset 11f8b03a88ad — Gerwin Klein <kleing@unsw.edu.au> / hgweb
adjust usage version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
set release version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
update release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
new entry Foundation_of_geometry — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
adjust for Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
new entry Simplicial_complexes_and_boolean_functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
adjust to Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
metadata and sitegen for Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
added Mathematics/Measure theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
New entry: Van_Emde_Boas_Trees — nipkow / hgweb
New entry: Van_Emde_Boas_Trees — nipkow / hgweb
metadata and sitegen for SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb

#82 (Dec 12, 2021, 12:14:00 AM)

provide component naproche-20211211; — wenzelm / hgweb
merged — wenzelm / hgweb
more Mailman archives; — wenzelm / hgweb
more Mailman content; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned metis to use map_index — desharna / hgweb
merged — desharna / hgweb
fixed HOL-TPTP — desharna / hgweb
tuned vars_of_iterm — desharna / hgweb
fixed TPTP generation of multi-arity expressions — desharna / hgweb
proper handling of Hilbert choice in TFX logics — desharna / hgweb
proper tptp_builtins — desharna / hgweb
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle — desharna / hgweb
proper proxy for Hilbert choice in TPTP output — desharna / hgweb
proper polymorphism for TH1 format in Sledgehammer — desharna / hgweb
refactored $ite and $let configuration and added dummy_thf_reduced prover — desharna / hgweb
tuned TPTP file names generated by Sledgehammer — desharna / hgweb
tuned SMT-Lib file names generated by Mirabelle — desharna / hgweb
added support for higher-order SMT proof search in Sledgehammer — desharna / hgweb
separated FOOL from $ite/$let in TPTP output — desharna / hgweb
missing latex font — nipkow / hgweb
Rewrite: added links to docu, made more prominent — nipkow / hgweb
discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
tuned proof; — wenzelm / hgweb
isabelle update_cartouches; — wenzelm / hgweb
more symbolic latex_output via XML (using YXML within text); — wenzelm / hgweb
tuned signature: remove unused; — wenzelm / hgweb
prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified corner cases of syntax; — wenzelm / hgweb
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2); — wenzelm / hgweb
a slightly simpler proof — paulson <lp15@cam.ac.uk> / hgweb

#82 (Dec 12, 2021, 12:14:00 AM)

merged — desharna / hgweb
generalized standard formula redundancy out of standard redundancy — desharna / hgweb
merged — wenzelm / hgweb
discontinued Parse.text; — wenzelm / hgweb
discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
weakened locale assumptions: wfP implies asymp — desharna / hgweb
Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
refactored Standard_Redundancy_Criterion to not use ordering type classes — desharna / hgweb
isabelle update_cartouches; — wenzelm / hgweb
removed obsolete "extend" operation; — wenzelm / hgweb
more symbolic latex_output via XML (using YXML within text);
re-use existing Latex.output_markup; — wenzelm / hgweb
prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
tuned signature; — wenzelm / hgweb

#81 (Dec 5, 2021, 12:14:00 AM)

provide component naproche-2d99afe5c349; — wenzelm / hgweb
merged — wenzelm / hgweb
Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2 — wenzelm / hgweb
more documentation about Type/Const antiquotations; — wenzelm / hgweb
more documentation about document build options; — wenzelm / hgweb
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c); — wenzelm / hgweb
tuned --- fewer IDE warnings; — wenzelm / hgweb
more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing; — wenzelm / hgweb
added definitions multp{DM,HO} and corresponding lemmas — desharna / hgweb
added wfP_less to wellorder and wfP_less_multiset — desharna / hgweb
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3 — desharna / hgweb
merged — desharna / hgweb
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset — desharna / hgweb
redefined less_multiset to be based on multp — desharna / hgweb
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp — desharna / hgweb
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max — desharna / hgweb
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp — desharna / hgweb
added lemma wfP_multp — desharna / hgweb
added lemma mono_multp — desharna / hgweb
added Multiset.multp as predicate equivalent of Multiset.mult — desharna / hgweb
address problems with launch4j and jdk-17 (see also 41d009462d3c); — wenzelm / hgweb
more robust build on midrange hardware; — wenzelm / hgweb
clarified tests: omit somewhat pointless (unstable) results; — wenzelm / hgweb
proper fields for gnuplot (amending b614e3e4146a); — wenzelm / hgweb
tuned output; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — wenzelm / hgweb
more robust build on midrange hardware (despite 67d6f1708ea4); — wenzelm / hgweb
Added tag Isabelle2021-1-RC4 for changeset 2336356d4180 — wenzelm / hgweb
updated to polyml-5.9; — wenzelm / hgweb
NEWS on "isabelle mirabelle"; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified default for kodkod_scala;
NEWS for proper release; — wenzelm / hgweb
maintain option kodkod_scala within theory context, to allow local modification; — wenzelm / hgweb
NEWS for proper release; — wenzelm / hgweb
updated to flatlaf-1.6.4; — wenzelm / hgweb
avoid broken links: auxiliary files are not yet supported; — wenzelm / hgweb
option document_comment_latex supports e.g. Dagstuhl LIPIcs; — wenzelm / hgweb
more explicit type Latex.Tags;
generate isabelletags.sty from Isabelle/Scala, including comment.sty setup; — wenzelm / hgweb
more uniform treatment of optional_argument for Latex elements;
discontinued somewhat pointless element position in Isabelle/Scala: semantic add-ons are better provided in Isabelle/ML;
clarified signature of class Latex: overridable unknown_elem allows to extend the markup language; — wenzelm / hgweb
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches; — wenzelm / hgweb
example: alternative document headings, based on more general document output markup; — wenzelm / hgweb
more general document output: enclosing markup is defined in user-space; — wenzelm / hgweb
clarified modules (see c299abcf7081); — wenzelm / hgweb
output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
tuned signature: more explicit types for presentation; — wenzelm / hgweb
more robust support for Windows line-endings; — wenzelm / hgweb
source positions for document markup commands, e.g. to retrieve PIDE markup in presentation; — wenzelm / hgweb
more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory; — wenzelm / hgweb
clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true"; — wenzelm / hgweb
more symbolic latex_output via XML (using YXML within text); — wenzelm / hgweb
proper enclose_name (amending e77c5bfca9aa); — wenzelm / hgweb
Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.; — wenzelm / hgweb
more symbolic latex_output via XML; — wenzelm / hgweb
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab); — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
updated to verit-2021.06.2-rmx; — wenzelm / hgweb
clarified HTML_Context.theory_exports: prefer value-oriented parallelism; — wenzelm / hgweb
generate problems with correct logic for veriT — fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
more parallelism, at the cost of potential duplicates of make_thy; — wenzelm / hgweb
afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a); — wenzelm / hgweb
more interrupts; — wenzelm / hgweb
present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
eliminated implicit state: these theories are globally unique; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
tuned (see also e0d1d9203275); — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
spelling; — wenzelm / hgweb

#81 (Dec 5, 2021, 12:14:00 AM)

feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
adjust for new tags in Isabelle2021-1-RC4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
fixed lemma following Isabelle/c256bba593f3 — desharna / hgweb
fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb

#80 (Nov 28, 2021, 12:14:00 AM)

added asymp_{less,greater} to preorder and moved mult1_lessE out — desharna / hgweb
renamed multp_code_iff and multeqp_code_iff — desharna / hgweb
simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0 — desharna / hgweb
renamed Multiset.multp and Multiset.multeqp — desharna / hgweb

#79 (Nov 21, 2021, 12:14:00 AM)

added lemmas — nipkow / hgweb
merged — wenzelm / hgweb
tuned; — wenzelm / hgweb
removed redundant test (see also 86fac52c2795, a9fea3f11cc0); — wenzelm / hgweb
just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow); — wenzelm / hgweb
proper version; — wenzelm / hgweb
back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834); — wenzelm / hgweb
less ambitious parallelism: more direct read/write saves overall heap space and GC time; — wenzelm / hgweb
slightly faster XML output: avoid too much regrowing of StringBuilder; — wenzelm / hgweb
updated NEWS: arm64-linux support is almost complete; — wenzelm / hgweb
update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9; — wenzelm / hgweb
more material for HOL-Analysis.Infinite_Sum — Manuel Eberl <manuel@pruvisto.org> / hgweb
more symbolic latex_output via XML; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
updated to polyml-5.9-610a153b941d -- close to final; — wenzelm / hgweb
tuned signature (again): latex_output is likely to depend on context; — wenzelm / hgweb
more symbolic latex output;
discontinued Latex.output_text, which is in conflict with symbolic output; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
symbolic latex_output via XML, interpreted in Isabelle/Scala; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature: more privacy; — wenzelm / hgweb
tuned output --- less redundancy; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
clarified signature: Latex.Output as parameter to Document_Build.Engine;
tuned; — wenzelm / hgweb
proper detection of ARM platform variants; — wenzelm / hgweb
back to post-release mode; — wenzelm / hgweb
updated for release; — wenzelm / hgweb
Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5 — wenzelm / hgweb
merged — wenzelm / hgweb
updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default); — wenzelm / hgweb
clarified HTML_Context: more explicit directory structure; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified properties: avoid empty entry; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb

#79 (Nov 21, 2021, 12:14:00 AM)

A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself — Dominique Unruh <unruh@ut.ee> / hgweb
Elimination of all z3 calls — paulson <lp15@cam.ac.uk> / hgweb
Word_Lib sync from l4v; tweak word_eqI — Gerwin Klein <kleing@unsw.edu.au> / hgweb
generalise word_eqI method; make sure it is exercised — Gerwin Klein <kleing@unsw.edu.au> / hgweb
test_bit_size not longer needed; avoid potential nontermination — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Word_Lib tweaks for slightly more backwards compatibility — Gerwin Klein <kleing@unsw.edu.au> / hgweb
use bit_simps in word_eqI method — Gerwin Klein <kleing@unsw.edu.au> / hgweb
adapted to new version of Infinite_Sum in isabelle-dev — Manuel Eberl <eberlm@in.tum.de> / hgweb
avoid hardwired document output; — wenzelm / hgweb
CTR and ETTS: integration with SpecCheck: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
merge — Burkhart Wolff <wolff@lri.fr> / hgweb
merge — Burkhart Wolff <wolff@lri.fr> / hgweb
Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc. — Burkhart Wolff <wolff@lri.fr> / hgweb
documentation fine-tuning. — Burkhart Wolff <wolff@lri.fr> / hgweb
Added section on C11_Ast_Lib in chapter II. — Burkhart Wolff <wolff@lri.fr> / hgweb
Example section restored and Documentation adapted. — Burkhart Wolff <wolff@lri.fr> / hgweb
Stramge intermediate configuration: Example section zerschossen. — Burkhart Wolff <wolff@lri.fr> / hgweb
Port to Isabelle2021-1 RC 2. — Burkhart Wolff <wolff@lri.fr> / hgweb
Improved documentation. — Burkhart Wolff <wolff@lri.fr> / hgweb
Examples for iterator - applications: queries, and translations into term. — Burkhart Wolff <wolff@lri.fr> / hgweb
Rearranging standard root store; better documentation in C_Command. — Burkhart Wolff <wolff@lri.fr> / hgweb
Rearranging the ML _programming Example Section C1. — Burkhart Wolff <wolff@lri.fr> / hgweb
reorg 1 — Burkhart Wolff <wolff@lri.fr> / hgweb
... — Burkhart Wolff <wolff@lri.fr> / hgweb
Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy) — Burkhart Wolff <wolff@lri.fr> / hgweb
Restructuring of Interfaces; more show cases. — Burkhart Wolff <wolff@lri.fr> / hgweb
Updated meta-data for Optics — Simon Foster <simon.foster@york.ac.uk> / hgweb
Additional scene laws — Simon Foster <simon.foster@york.ac.uk> / hgweb
Branch merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables. — Simon Foster <simon.foster@york.ac.uk> / hgweb
feat(SpecCheck/Show) add parentheses for option SOME case — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
merged — desharna / hgweb
weakened ordering requirements — desharna / hgweb
used well-founded pre-order in standard redundancy criterions — desharna / hgweb
derived refutational completeness from finitary and non-finitary standard redundancy criterion — desharna / hgweb
merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, since
they are now available as complete methods in Factor-Algebraic-Polynomial — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
factor_complex_poly delivers distinct list — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
merged — paulson / hgweb
Removal of material that's going to be in Isabelle2021-1 — paulson <lp15@cam.ac.uk> / hgweb
merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
refactoring (moving theories and lemmas around) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sync from l4v — Gerwin Klein <kleing@unsw.edu.au> / hgweb
adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
merge of afp-2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry PAL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
new entry Factor_Algebraic_Polynomial — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
document `publish -` — Gerwin Klein <kleing@unsw.edu.au> / hgweb
changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
changed affiliation of Eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
sitegen for Real_Power — paulson <lp15@cam.ac.uk> / hgweb
new entry Real_Power — paulson <lp15@cam.ac.uk> / hgweb
New entry Szemeredi_Regularity — nipkow / hgweb
tuned proofs -- avoid z3; — wenzelm / hgweb

#78 (Nov 14, 2021, 12:14:00 AM)

merged — nipkow / hgweb
tuned (thanks to J. Villadsen) — nipkow / hgweb
added padding to Mirabelle's output — desharna / hgweb
merged — desharna / hgweb
tuned generation of TPTP with $ite/$let in higher-order logics — desharna / hgweb
tuned generation of TPTP with $ite in function position — desharna / hgweb
tuned TPTP generation of If helper facts — desharna / hgweb
merged — wenzelm / hgweb
clarified signature: prefer static operations; — wenzelm / hgweb
clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources; — wenzelm / hgweb
more robust; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature: more explicit class Entity_Context with private state + operations; — wenzelm / hgweb
more hyperlinks, notably internal fact references; — wenzelm / hgweb
Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO — paulson <lp15@cam.ac.uk> / hgweb
A tiny bit of tidying connected with Zorn's Lemma — paulson <lp15@cam.ac.uk> / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition); — wenzelm / hgweb
revert temporary workaround 6d111935299c; — wenzelm / hgweb
added lemma — nipkow / hgweb
merged — nipkow / hgweb
tuned attributes to avoid looping — nipkow / hgweb
added eq_iff_swap for creating symmetric variants of thms; applied it in List. — nipkow / hgweb
tuned text; — wenzelm / hgweb
more robust timeout, following df4449c6eff1; — wenzelm / hgweb
more accurate Files.isRegularFile, exclude directories (e.g. jar_path); — wenzelm / hgweb
proper java_version for isabelle_setup; — wenzelm / hgweb
explicit option metric_argo_timeout, with reasonable default for Raspberry Pi; — wenzelm / hgweb
tuned; — wenzelm / hgweb
repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process); — wenzelm / hgweb
discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do; — wenzelm / hgweb
clarified messages, depending on option "document_echo"; — wenzelm / hgweb
just one cache, via HTML_Context, via Sessions.Store or Session; — wenzelm / hgweb
merged — paulson / hgweb
new lemmas about convex, concave functions, + tidying — paulson <lp15@cam.ac.uk> / hgweb
proper support for arm64; — wenzelm / hgweb
no perl (amending 59ef23ac81ab); — wenzelm / hgweb
merged — wenzelm / hgweb
Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b — wenzelm / hgweb
merged — nipkow / hgweb
Preserve variable name z in VAR {z = t} — nipkow / hgweb
back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin; — wenzelm / hgweb
updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default); — wenzelm / hgweb
more precise URL — nipkow / hgweb
tuned page breaks — nipkow / hgweb

#78 (Nov 14, 2021, 12:14:00 AM)

CTR and ETTS: integration with SpecCheck — user9716869 <user9716869@gmail.com> / hgweb
used antiquotation to fix LaTeX failure — desharna / hgweb
adapted to devel — nipkow / hgweb
updated to devel — nipkow / hgweb
merged — nipkow / hgweb
tuned proof for devel — nipkow / hgweb
clarified quotes vs. apostrophes vs. primes; — wenzelm / hgweb
more accurate use of LaTeX ndash; — wenzelm / hgweb
prefer portable LaTeX mdash; — wenzelm / hgweb
tuned whitespace --- removed suspicious Unicode; — wenzelm / hgweb
proper Unix linefeeds; — wenzelm / hgweb
changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
changed affiliation of eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
added author to Saturation_Framework_Extensions — desharna / hgweb
derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy — desharna / hgweb
added locale calculus_with_finitary_standard_redundancy — desharna / hgweb
Registers:
- Added mechanism for raising errors if autogenerated files need updating
- Changed definition of Axioms_Quantum.register_pair (returns 0 for incompatible registers, see register_pair_is_register_converse for a useful consequence)
- Slightly reducing namespace pollution in Classical_Extra (hiding consts x, y, X, Y etc.) — Dominique Unruh <unruh@ut.ee> / hgweb
feat(SpecCheck) add better unit tests facilities, examples and exceptions property — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author); — wenzelm / hgweb
Correctness_Algebras: increase nitpick timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
CZH: dagger monoidal categories — user9716869 <user9716869@gmail.com> / hgweb
update it Isabelle/925b46043b84 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
sitegen for Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#77 (Nov 7, 2021, 12:14:00 AM)

cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f); — wenzelm / hgweb
proper foundational order; — wenzelm / hgweb
back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition"; — wenzelm / hgweb
use all entity kinds from theory export, e.g. "method", "attribute"; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified physical_ref; — wenzelm / hgweb
proper treatment of session build hierarchy; — wenzelm / hgweb
proper used_theories for session build hierarchy, not known_theories from imported sessions; — wenzelm / hgweb
present theories from imported sessions as required; — wenzelm / hgweb
avoid multiple copies of fonts;
proper fonts prefix for aux. files; — wenzelm / hgweb
more compact persistent data; — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper term_cache; — wenzelm / hgweb
prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti; — wenzelm / hgweb
tuned; — wenzelm / hgweb
observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified order: prefer bottom-up construction of partial content; — wenzelm / hgweb
more thorough update_global_index: overwrite old content; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified HTML_Context: just one context type; — wenzelm / hgweb
unused (see also 217e6cf61453, 5e7916535860); — wenzelm / hgweb
merged — wenzelm / hgweb
clarified Theory_Cache: prefer immutable data with Synchronized variable;
clarified Export_Theory.Theory vs. Entity tables;
entity_ref: proper treatment of entity kind; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
unused; — wenzelm / hgweb
proper support of verit's return code for timeout — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
tuned whitespace; — wenzelm / hgweb
updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14"; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
prefer official Export.explode_name;
avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl; — wenzelm / hgweb
tuned; — wenzelm / hgweb
avoid conflict with future keyword; — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
clarified signature: more direct XML.symbol_length; — wenzelm / hgweb
more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it; — wenzelm / hgweb
tuned -- eliminate clones stemming from d28a51dd9da6; — wenzelm / hgweb
more to ANNOUNCE; — wenzelm / hgweb
clarified link style: similar to Isabelle/jEdit; — wenzelm / hgweb
tuned; — wenzelm / hgweb
improved HTML presentation by Fabian Huch; — wenzelm / hgweb
proper HTTPS; — wenzelm / hgweb
proper markup type (amending be49c660ebbf); — wenzelm / hgweb
merged; — wenzelm / hgweb
more PIDE markup; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more PIDE markup; — wenzelm / hgweb
recover library_index_content.template from c337c798f64c: required for website/build/main; — wenzelm / hgweb
merged — paulson / hgweb
simplified some ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
more generous timeout: support build on Raspberry Pi; — wenzelm / hgweb
add documentation for pred_mono — traytel / hgweb
merged — desharna / hgweb
added "mono" attribute to BNF generated pred_mono theorems — desharna / hgweb
merged — desharna / hgweb
do not declare $let-bound variables in TPTP output — desharna / hgweb
IDE build actually works (but somewhat pointless); — wenzelm / hgweb
suppress sources from jEdit/test, which prevent regular build of the generated scala_project; — wenzelm / hgweb
removed junk; — wenzelm / hgweb
improve pagebreaks by *not* using supertabular too much; — wenzelm / hgweb
updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc; — wenzelm / hgweb
more robust "isabelle scala_project": Gradle has been replaced by Maven; — wenzelm / hgweb
tuned; — wenzelm / hgweb
support linux_arm as well, e.g. native Docker on Apple Silicon; — wenzelm / hgweb
update paths at TUM; — wenzelm / hgweb
Added tag Isabelle2021-1-RC1 for changeset 81cc8f2ea9e7 — wenzelm / hgweb
updated for release; — wenzelm / hgweb
some reordering for release; — wenzelm / hgweb
updated to jdk-17.0.1+12; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
tuned; — wenzelm / hgweb
minor performance tuning; — wenzelm / hgweb
more robust; — wenzelm / hgweb
provide native executables for arm64-darwin, for more robust startup without Rosetta 2; — wenzelm / hgweb
tuned proofs -- avoid z3, which is unavailable on arm64-linux; — wenzelm / hgweb
prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb
discontinued pointless check of kodkodi_version, it is implicit in the bundled component; — wenzelm / hgweb

#77 (Nov 7, 2021, 12:14:00 AM)

Correctness_Algebras: increase session timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
tuned signature, according to Isabelle/df12779c3ce8; — wenzelm / hgweb
feat(SpecCheck) add possibility to make builds fail on failure and extend README — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
added missing funding information — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
restored theory structure for simple genericity. — haftmann / hgweb
Backed out changeset af549be0a8cd — haftmann / hgweb
restored different entrance points a before Isabelle2021 — haftmann / hgweb
proper parentheses (amending 354560d7143a); — wenzelm / hgweb
Adjusted to prospective release Isabelle2021-2. — haftmann / hgweb
Correctness_Algebras: uncomment counterexamples — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead; — wenzelm / hgweb
clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead; — wenzelm / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
remove unused functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
silence sitegen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
new entry X86_Semantics — Gerwin Klein <kleing@unsw.edu.au> / hgweb
adjust to isabelle@549019b4a808 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
metadata for Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
New entry Correctness_Algebras — nipkow / hgweb
prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb

#76 (Oct 31, 2021, 12:14:00 AM)

tuned proofs -- avoid z3, which is unavailable on arm64-linux; — wenzelm / hgweb
tuned; — wenzelm / hgweb
test version of prespective polyml-5.9; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
updated for pre-5.9 testing; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
more robust subgoal addressing; — wenzelm / hgweb
proper subgoal addressing; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
recursive find_eq, not find_dist; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
order_tac: prevent potential bug, improve perf and tracing

- We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p. — Lukas Stevens <mail@lukas-stevens.de> / hgweb
misc tuning and clarification; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; — wenzelm / hgweb
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; — wenzelm / hgweb
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570); — wenzelm / hgweb
added Thm.instantiate_beta;
tuned; — wenzelm / hgweb
moved generic implementation into HOL-Main — haftmann / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
discontinued somewhat pointless antiquotations; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
support for "lemma";
support for "schematic" mode;
clarified error position; — wenzelm / hgweb
tuned; — wenzelm / hgweb
local fixes for "lemma" antiquotation; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified keywords: major take precedence for commands, but not used for antiquotations;
clarified modules; — wenzelm / hgweb
tuned modules; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
moved a theorem to a sensible place — paulson <lp15@cam.ac.uk> / hgweb
merged — wenzelm / hgweb
tuned, continuing e955964d89cb; — wenzelm / hgweb
avoid waste of resources due to dynamic simpset (amending 45c09620f726); — wenzelm / hgweb
fix latex — Norbert Schirmer <nschirmer@apple.com> / hgweb
clarified modules; — wenzelm / hgweb
more generic bit/word lemmas for distribution — haftmann / hgweb
merged — paulson / hgweb
Added / moved some simple set-theoretic lemmas — paulson <lp15@cam.ac.uk> / hgweb
more CONTRIBUTORS and NEWS; — wenzelm / hgweb
cleanup; add Apple reference — Norbert Schirmer <nschirmer@apple.com> / hgweb
refine interface — Norbert Schirmer <nschirmer@apple.com> / hgweb
generalized component lookup for syntax and distinctness proofs. added some tracing. — Norbert Schirmer <nschirmer@apple.com> / hgweb
merged — wenzelm / hgweb
tuned; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more robust: genuinely free variables need to be instantiated; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
clarified errors; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature -- avoid clones; — wenzelm / hgweb
Refinement of partitions — paulson <lp15@cam.ac.uk> / hgweb
avoid persistence of static context: instantiation arguments should provide proper dynamic context; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more markup; — wenzelm / hgweb
clarified name, syntax, messages; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more control symbols; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
ML antiquotations to instantiate types/terms/props; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified keywords and reports; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
merged — desharna / hgweb
proper veriT --max-time option — desharna / hgweb
refactored tptp_builtins in Sledgehammer — desharna / hgweb
merged — wenzelm / hgweb
tuned ML --- clarified use of context;
tuned message; — wenzelm / hgweb
tuned --- fewer clones; — wenzelm / hgweb
updated to jEdit plugin Highlight 2.5; — wenzelm / hgweb
proper tactic combinator; — wenzelm / hgweb
proper file headers; — wenzelm / hgweb
clarified context;
clarified modules; — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
updated email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
removed some 'private' modifiers from HOL-Computational_Algebra — Manuel Eberl <manuel@pruvisto.org> / hgweb
merged — wenzelm / hgweb
merged — wenzelm / hgweb
more robust Variable.revert_bounds (see also b12f2cef3ee5); — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
tuned -- proper names/scopes for contexts; — wenzelm / hgweb
clarified context; — wenzelm / hgweb
clarified context; — wenzelm / hgweb
tuned; — wenzelm / hgweb
unused; — wenzelm / hgweb
more accurate treatment of context;
declare generated bounds for the sake of recdef, which has variables leaking from local context; — wenzelm / hgweb
isabelle regenerate_cooper; — wenzelm / hgweb
revert bbfed17243af, breaks HOL-Proofs extraction; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper p' instead of p (amending 52c7c42e7e27); — wenzelm / hgweb
proper context for Goal.prove_internal; — wenzelm / hgweb
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Simplifier and equational conversions demand a proper proof context; — wenzelm / hgweb
more accurate treatment of context, notably for nested Goal.proof / SUBPROOF; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
spelling; — wenzelm / hgweb
clarified context; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned Vampire configuration to use TFX in Sledgehammer — desharna / hgweb

#76 (Oct 31, 2021, 12:14:00 AM)

updated metadata for Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
corrected the timeout for CZH_Universal_Constructions — user9716869 <user9716869@gmail.com> / hgweb
CZH: further results about comma categories and Kan extensions, a variety of other minor amendments — user9716869 <user9716869@gmail.com> / hgweb
more generic bit/word lemmas for distribution — haftmann / hgweb
Fixing a name clash between two different "restrict" operators — paulson <lp15@cam.ac.uk> / hgweb
Merged — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
solved the roots-on-the-border problem — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
split Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
more realistic timeout; — wenzelm / hgweb
clarified signature, according to Isabelle/ccf599864beb; — wenzelm / hgweb
back to dedicated separate shift operations for infix syntax;
more default simp rules on closed numeric expressions — haftmann / hgweb
modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
Various tuning that for some reason didn't get merged from my master branch. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
A spot of polishing — paulson <lp15@cam.ac.uk> / hgweb
Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
Update metadata to reflect changes made in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
Add a revision note concerning material added in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
tuned signature, according to Isabelle/042041c0ebeb; — wenzelm / hgweb
Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
Adjust Imperative List/Map/Set Specification for more lenient next operation

This allows implementations of this iterator specification to make use of
temporary variables for obtaining the next element of the list/set/map.
This is required by some and especially more general iterators. — n.muendler <n.muendler@tum.de> / hgweb
discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
metadata update for MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
fixed a mistake in MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
adjusted Virtual-Substitution from 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
fixed duplicate "and" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sitegen for Virtual_Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Virtual Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
updated website/email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
modifications in Jinja and DOminance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
merged — wenzelm / hgweb
adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
tuned -- proper names/scopes for contexts; — wenzelm / hgweb
tuned proofs; — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
more accurate treatment of context; — wenzelm / hgweb
proper antiquotations; — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
tuned whitespace; — wenzelm / hgweb
dead code!? — wenzelm / hgweb
clarified signature, following Isabelle/de4f151c2a34; — wenzelm / hgweb

#75 (Oct 24, 2021, 12:14:00 AM)

added Mirabelle action presburger — desharna / hgweb
added timing to Mirabelle action arith — desharna / hgweb
added error message on invalid Mirabelle action — desharna / hgweb

#75 (Oct 24, 2021, 12:14:00 AM)

CZH: large limits, generalizations, a variety of minor amendments — user9716869 <user9716869@gmail.com> / hgweb

#74 (Oct 17, 2021, 12:14:00 AM)

A few new lemmas plus some refinements — paulson <lp15@cam.ac.uk> / hgweb
merged — desharna / hgweb
produced Mirabelle output directly in ML until Scala output gets fixed — desharna / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
removed unused material (left-over from fd0c85d7da38); — wenzelm / hgweb
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a); — wenzelm / hgweb
removed junk; — wenzelm / hgweb
merged — nipkow / hgweb
separated commands from annotations to be able to abstract about the latter only — nipkow / hgweb
prefer standard Term.dest_abs, with minor deviation of generated names; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
more examples — nipkow / hgweb
workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't; — wenzelm / hgweb
more complete simp rules — haftmann / hgweb
more complete simp rules — haftmann / hgweb
avoid overaggressive contraction of conversions — haftmann / hgweb
normalizing NOT (numeral _) (again) — haftmann / hgweb

#74 (Oct 17, 2021, 12:14:00 AM)

Simplified a definition — paulson <lp15@cam.ac.uk> / hgweb
modify propa — nanjiang <nanjiang@whu.edu.cn> / hgweb
bit singleton shifts recovered for the sake of backward compatibility — haftmann / hgweb
updated to 7422950f3955 — nipkow / hgweb
merge — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
EPO: simplify proof — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
primer — haftmann / hgweb
more complete simp rules — haftmann / hgweb
more complete simp rules (examples) — haftmann / hgweb
avoid overaggressive contraction of conversions — haftmann / hgweb
slightly more prominence for proof tools; more examples — haftmann / hgweb

#73 (Oct 10, 2021, 12:14:00 AM)

tuned text; — wenzelm / hgweb
recover NEWS from 78d1f73bbeaa; — wenzelm / hgweb
save 90 MB by excluding rlwrap and thus perl; — wenzelm / hgweb
save 45 MB by excluding rlwrap and thus perl; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
clarified test of directories; — wenzelm / hgweb
misc tuning for release; — wenzelm / hgweb
merged — wenzelm / hgweb
updated to kodkodi-1.5.7. with more robust/portable management of files and processes; — wenzelm / hgweb
provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
proper build on macOS; — wenzelm / hgweb
build minisat, using recent fork from original sources; — wenzelm / hgweb
proper platform_path for executables run from Java; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
merged — desharna / hgweb
added timeout to veriT — desharna / hgweb
new notion of infinite sums in HOL-Analysis, ordering on complex numbers — eberlm <eberlm@in.tum.de> / hgweb
NEWS and CONTRIBUTORS — desharna / hgweb
merged — desharna / hgweb
added offset to Mirabelle's tptp output names — desharna / hgweb
tuned zipperposition config in sledgehammer — desharna / hgweb
considered slices overhead in sledgehammer — desharna / hgweb
tuned atp_prover sliding — desharna / hgweb
tuned Zipperposition slides in sledgehammer — desharna / hgweb
include arm64-linux; — wenzelm / hgweb
updated to Vampire 4.6, as proposed by Martin Desharnais; — wenzelm / hgweb
build from official downloads; — wenzelm / hgweb
build just one vampire version; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche; — wenzelm / hgweb
more exports, notably for Isabelle/Naproche; — wenzelm / hgweb
include arm64-linux; — wenzelm / hgweb
prefer existing OCaml installation; — wenzelm / hgweb
include arm64-linux; — wenzelm / hgweb
no patchelf on macOS (undetected due to cached executables?); — wenzelm / hgweb
provide opam-2.1.0 for experimentation; — wenzelm / hgweb
rebuild cygwin-20211004.tar.gz; — wenzelm / hgweb
include arm64-linux; — wenzelm / hgweb
updated to cygwin-20211004: build again; — wenzelm / hgweb
merged — wenzelm / hgweb
removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default; — wenzelm / hgweb
actually use cygwin-20211002 (amending ff0ca375457c); — wenzelm / hgweb
discontinued perl; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
proper term operation Term.dest_abs; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned proofs;
fewer warnings; — wenzelm / hgweb
more standard binder syntax; — wenzelm / hgweb
clarified 'let' syntax: avoid conflict with existing 'let' in FOL; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — paulson / hgweb
removal of a redundant theorem (and white space) — paulson <lp15@cam.ac.uk> / hgweb
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions — paulson <lp15@cam.ac.uk> / hgweb
clarified and updated for release; — wenzelm / hgweb
formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc; — wenzelm / hgweb
more NEWS and CONTRIBUTORS; — wenzelm / hgweb
clarified comments; — wenzelm / hgweb
support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing); — wenzelm / hgweb
clarified dependencies; — wenzelm / hgweb
updated for release; — wenzelm / hgweb
Added tag Isabelle2021-1-RC0 for changeset fedc0b659881 — isatest / hgweb
provide Isabelle/jEdit plugins as services, and thus allow user components do the same; — wenzelm / hgweb
merged — wenzelm / hgweb
updated for release; — wenzelm / hgweb
misc tuning for release; — wenzelm / hgweb
update dependency; — wenzelm / hgweb
trim whitespace; — wenzelm / hgweb
misc tuning for release; — wenzelm / hgweb
misc tuning for release; — wenzelm / hgweb
isabelle build_components -u; — wenzelm / hgweb
updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7; — wenzelm / hgweb
updated to current Cygwin, near 3.2.0;
discontinued perl; — wenzelm / hgweb
updated to sumatra_pdf-3.3.3; — wenzelm / hgweb
updated default version; — wenzelm / hgweb
updated to xz-java-1.9; — wenzelm / hgweb
updated to sqlite-jdbc-3.36.0.3; — wenzelm / hgweb
updated to postgresql-42.2.24; — wenzelm / hgweb
updated to jfreechart-1.5.3; — wenzelm / hgweb
updated to flatlaf-1.6; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax; — wenzelm / hgweb
clarified sledgehammer_provers, following d8dc8fdc46fc; — wenzelm / hgweb
proper term operation Term.dest_abs; — wenzelm / hgweb
tuned, following Syntax_Trans.variant_abs; — wenzelm / hgweb
proper patterns for (- numeral t), amending 03ff4d1e6784; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
update syntax for verit — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
provide verit-2021.06-rmx; — wenzelm / hgweb

#73 (Oct 10, 2021, 12:14:00 AM)

ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
CTR and ETTS: integration with fd5f62176987 — user9716869 <user9716869@gmail.com> / hgweb
adapted QHLProver to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
adapted to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
adapted to devel — nipkow / hgweb
Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Weighted_Path_Order: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
add missing session dependency — Gerwin Klein <kleing@unsw.edu.au> / hgweb
new entry FOL_Axiomatic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
minor editorial changes for CZH entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
New entry Weighted_Path_Order — nipkow / hgweb
fxed metadata (forgot .html) in link — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
metadata and sitegen for complex bounded operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Complex_Bounded_Operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; — wenzelm / hgweb
clarified timeout;
tuned whitespace; — wenzelm / hgweb
hide_lams ~> opaque_lifting; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
proper inst table; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
proper inst table; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
unused; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
proper match against const_name; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
fix(ci): clarified addresses, set proper TLS version; — Fabian Huch <huch@in.tum.de> / hgweb
feat(ci): remove hard-coded address; — Fabian Huch <huch@in.tum.de> / hgweb
feat(SpecCheck/Show) tune pretty printing for environments — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entries by Mihails Milehins

CZH_Elementary_Categories, CZH_Foundations,
CZH_Universal_Constructions, Conditional_Simplification,
Conditional_Transfer_Rule, Intro_Dest_Elim, and Types_To_Sets_Extension — Gerwin Klein <kleing@unsw.edu.au> / hgweb
New entry: Dominance_CHK — nipkow / hgweb
Schutz_Spacetime website — paulson <lp15@cam.ac.uk> / hgweb
new entry Schutz_Spacetime — paulson <lp15@cam.ac.uk> / hgweb
metadata for Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#72 (Oct 3, 2021, 12:14:00 AM)

clarified antiquotations; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified antiquotations;
some comments concerning odd "- numeral"; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
merged — desharna / hgweb
tuned TPTP parsing of THF function application — desharna / hgweb
clarified examples; — wenzelm / hgweb
repaired slip — haftmann / hgweb
merged — desharna / hgweb
updated to Zipperposition 2.1 — desharna / hgweb
fixed veriT environment variable in sledgehammer's documentation — desharna / hgweb
avoid overlapping PIDE markup (amending bb25ea271b15); — wenzelm / hgweb
recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB); — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified positions, notably for ML compiler errors; — wenzelm / hgweb
clarified message; — wenzelm / hgweb
proper default for Sledgehammer GUI panel; — wenzelm / hgweb
tuned antiquotations; — wenzelm / hgweb
more convenient ML arguments: avoid excessive nesting of cartouches; — wenzelm / hgweb
outer syntax: support for control-cartouche tokens; — wenzelm / hgweb
merged — nipkow / hgweb
An example — nipkow / hgweb
prefer veriT over Z3 in sledgehammer — desharna / hgweb
added Zipperposition to sledgehammer's default provers — desharna / hgweb
provide zipperposition-2.1 (still unused); — wenzelm / hgweb
tuned docs — blanchet / hgweb
merged — wenzelm / hgweb
improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; — wenzelm / hgweb
NOT is part of syntax bundle also — haftmann / hgweb

#72 (Oct 3, 2021, 12:14:00 AM)

repaired slip — haftmann / hgweb
feat(SpecCheck) folder renaming, types for tests — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
tuned — nipkow / hgweb
mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f; — wenzelm / hgweb

#71 (Sep 26, 2021, 12:14:00 AM)

merged — wenzelm / hgweb
tuned proofs --- avoid 'guess'; — wenzelm / hgweb
apply declarations from interpretations in eigen context also — haftmann / hgweb
grant access to sun.tools.jconsole, as required for Java 17; — wenzelm / hgweb
update to e-2.6, following Martin Desharnais; — wenzelm / hgweb
updated to Metis 2.4 (release 20200713) — desharna / hgweb
avoid problems with launch4j and jdk-17; — wenzelm / hgweb
update to jdk-17+35 (LTS); — wenzelm / hgweb
tuned message; — wenzelm / hgweb
unused since 398b7bb9ebdd; — wenzelm / hgweb
merged — desharna / hgweb
removed checks for non-commercial usage of Vampire as it is now under BSD licence — desharna / hgweb
enabled FOOL for Vampire in Sledgehammer — desharna / hgweb
used Vampire 4.5.1 in Sledgehammer — desharna / hgweb
proper NEWS; — wenzelm / hgweb
tuned NEWS; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified partial application: immediate check of object-logic, and avoidance of context within closure; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
ML antiquotations for object-logic judgment; — wenzelm / hgweb
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
more uniform syntax; — wenzelm / hgweb
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; — wenzelm / hgweb
localized command 'syntax' and 'no_syntax'; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
merged — desharna / hgweb
proper constants in TPTP $let binding — desharna / hgweb
more operations from Isabelle/ML; — wenzelm / hgweb
merged — wenzelm / hgweb
tuned proofs --- eliminated 'guess'; — wenzelm / hgweb
tuned proofs;
tuned whitespace; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
proper firstorderization in Sledgehammer — desharna / hgweb
clarified signature;
clarified antiquotations; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
clarified signature -- prefer antiquotations (with subtle change of exception content); — wenzelm / hgweb
more control symbols; — wenzelm / hgweb
support ML antiquotations with fn abstraction; — wenzelm / hgweb
unused; — wenzelm / hgweb

#71 (Sep 26, 2021, 12:14:00 AM)

ported Design-Theory from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
ported Three-Circles from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
ported Cubic_Quartic_Equations from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
Cubic_Quartic_Equations sitegen — paulson <lp15@cam.ac.uk> / hgweb
new entry Cubic_Quartic_Equations — paulson <lp15@cam.ac.uk> / hgweb
sitegen for combinatorial design theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Combinatorial Design Theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sitegen for Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
clarified modules, according to Isabelle/534b231ce041; — wenzelm / hgweb
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax, according to Isabelle/ead56ad40e15;
subtle change of inf (infixl "\<sqinter>" 70) vs. (infixl "\<sqinter>" 65); — wenzelm / hgweb
clarified signature, according to Isabelle/d882abae3379; — wenzelm / hgweb

#70 (Sep 19, 2021, 12:14:00 AM)

clarified operations: follow Isabelle/ML more closely; — wenzelm / hgweb
provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche; — wenzelm / hgweb
obsolete; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified name and options for old vampire-4.2.2; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
more latex macros; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations;
more formal use of consts; — wenzelm / hgweb
more antiquotations;
more formal use of consts; — wenzelm / hgweb
clarified antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
clarified antiquotation; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb
tuned; — wenzelm / hgweb
ML antiquotations for type constructors and term constants; — wenzelm / hgweb
more antiquotations; — wenzelm / hgweb

#70 (Sep 19, 2021, 12:14:00 AM)

explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
tuned signature, according to Isabelle/28a582aa25dd; — wenzelm / hgweb

#69 (Sep 12, 2021, 12:14:00 AM)

tuned; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
miscellaneous examples and experiments for Isabelle/Pure; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
unused; — wenzelm / hgweb
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference); — wenzelm / hgweb
NEWS; — wenzelm / hgweb
clarified signature: more scalable operations; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
clarified order of extra type variables, following names more often than occurrences; — wenzelm / hgweb
clarified signature;
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
more robust: client could have terminated already; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified set of items with order of addition; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
clarified signature;
clarified modules; — wenzelm / hgweb
tuned; — wenzelm / hgweb
simplified: uniqueness check happens in export_consumer; — wenzelm / hgweb
more markup, e.g. to locate defining theory node in formal document output; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
export other entities, e.g. relevant for formal document output;
clarified markup kind (PIDE) vs. export kind (e.g. MMT); — wenzelm / hgweb
pointer_eq_ord: minor performance tuning; — wenzelm / hgweb
more robust: progress.stopped means that build has failed; — wenzelm / hgweb
more reactive interrupt; — wenzelm / hgweb
more reactive interrupt; — wenzelm / hgweb
more robust: retain length of results; — wenzelm / hgweb
more reactive interrupt; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified signature;
minor performance tuning; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
unused; — wenzelm / hgweb
more efficient operations: traverse hyps only when required; — wenzelm / hgweb
more robust signature: result has no particular order; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
unused; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
clarified; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
more scalable operations;
tuned; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
white space — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
some fixes connected with card_Diff_singleton — paulson <lp15@cam.ac.uk> / hgweb
strengthened a few lemmas about finite sets and added a code equation for complex_of_real — paulson <lp15@cam.ac.uk> / hgweb
tuned; — wenzelm / hgweb
proper inst table; — wenzelm / hgweb
more scalable data structure (but: rarely used many arguments); — wenzelm / hgweb
minor performance tuning: fewer allocations;
clarified theory context; — wenzelm / hgweb

#69 (Sep 12, 2021, 12:14:00 AM)

eliminated Specification.definition', following Isabelle/6876e3d5e362; — wenzelm / hgweb
clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a; — wenzelm / hgweb
clarified signature, according to Isabelle/612b7e0d6721; — wenzelm / hgweb
tuned signature, according to Isabelle/839a6e284545; — wenzelm / hgweb
merged — sterraf / hgweb
Backed out changeset ef19e4e58b8c
restoring old argument order on synthesized formulas — sterraf / hgweb
avoid hardwired document; — wenzelm / hgweb
merged — wenzelm / hgweb
tuned signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
simplified, using Isabelle/ML operations; — wenzelm / hgweb
adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
more scalable operations; — wenzelm / hgweb
merged — sterraf / hgweb
synthesized formulas have their variables permuted — sterraf / hgweb
merged — paulson / hgweb
fixes for cardinality lemmas — paulson <lp15@cam.ac.uk> / hgweb
proper inst table; — wenzelm / hgweb

#68 (Sep 5, 2021, 12:14:00 AM)

tuned; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
more Isabelle/Haskell operations;
tuned; — wenzelm / hgweb
avoid change of existing file, notably rebuild via ghc_stack; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
clarified process description; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb

#67 (Aug 29, 2021, 12:14:00 AM)

more Isabelle/Haskell; — wenzelm / hgweb
made sure lambda-lifting works well with native let binders in Sledgehammer — blanchet / hgweb
handle Zipperposition's ResourceOut gracefully — blanchet / hgweb
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax — blanchet / hgweb
proper test for type constructor; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
merged — wenzelm / hgweb
tuned; — wenzelm / hgweb
more scalable data structure (but: rarely used with > 5 arguments); — wenzelm / hgweb
Backed out changeset d4af818e0880 — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
merged — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
reflect moved theories — nipkow / hgweb
unhide canonical function def examples — nipkow / hgweb
merged — nipkow / hgweb
merged — nipkow / hgweb
Backed out changeset fe8d0f4da0e6 — nipkow / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
more Isabelle/Haskell operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
minor performance tuning; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
treat Symbol.eof as in ML (but: presently unused); — wenzelm / hgweb
tuned; — wenzelm / hgweb
minor performance tuning; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
proper Isabelle symbol positions; — wenzelm / hgweb
more Haskell operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature: prefer existing Haskell operations; — wenzelm / hgweb
more Haskell operations; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
tuned; — wenzelm / hgweb
consolidation of rules for bit operations — haftmann / hgweb

#67 (Aug 29, 2021, 12:14:00 AM)

Graphic rendering of Relational_Method PDF files refined. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
Entry Relational_Method updated. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
more realistic timeout; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
follow Isabelle/53e28c438f96; — wenzelm / hgweb
clarified signature, following Isabelle/a3b0fc510705; — wenzelm / hgweb
merged — nipkow / hgweb
tuned — nipkow / hgweb
consolidation of rules for bit operations — haftmann / hgweb

#66 (Aug 22, 2021, 12:14:00 AM)

fixed $ite syntax in TPTP TFX generation — desharna / hgweb
more Haskell operations; — wenzelm / hgweb
merged — wenzelm / hgweb
revert 0faa68dedce5: very slow; — wenzelm / hgweb
tuned; — wenzelm / hgweb
add/rename some theorems about Map(pings) — Lukas Stevens <mail@lukas-stevens.de> / hgweb
support configuration options "show_results"; — wenzelm / hgweb
consolidate_body more thoroughly, e.g. for reduced ML_Heap.obj_size; — wenzelm / hgweb
merged — desharna / hgweb
fixed $ite syntax in TPTP THX generation — desharna / hgweb
tuned signature; — wenzelm / hgweb
more scalable data structures; — wenzelm / hgweb
more scalable data structures; — wenzelm / hgweb
more scalable data structures;
tuned; — wenzelm / hgweb
proper position information for Context.theory_data_size; — wenzelm / hgweb

#66 (Aug 22, 2021, 12:14:00 AM)

tuned name — nipkow / hgweb
Fix typo — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
Tune references

... using new name of BD_Security_Compositional — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
Remove redundant license — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
more realistic timeout: approx. 5min CPU time; — wenzelm / hgweb
cleaning up — nipkow / hgweb
New entry CoSMeDis — nipkow / hgweb
New entry CoSMed — nipkow / hgweb
New entry: BD_Security_Compositional — nipkow / hgweb
New entry: CoCon — nipkow / hgweb
updated to devel — nipkow / hgweb
merge from AFP 2021 — nipkow / hgweb
New entry Fresh_Identifiers — nipkow / hgweb
New entry: Relational_Forests — nipkow / hgweb
cleaning up — nipkow / hgweb
merged — nipkow / hgweb
cleaning up — nipkow / hgweb
Update Bounded_Deducibility_Security

- Generalise BD Security from I/O automata to nondeterministic transition
systems, with the former retained as an instance of the latter (renaming
locale BD_Security to BD_Security_IO)
- Generalise unwinding conditions to allow making more than one transition at a
time when constructing alternative traces, giving more flexibility for
unwinding strategies
- Add various helper lemmas and definitions
- Add results about the expressivity of declassification triggers vs. bounds,
due to Thomas Bauereiss (added as author) — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
tuned signature, following Isabelle/069f6b2c5a07; — wenzelm / hgweb

#65 (Aug 15, 2021, 12:14:00 AM)

provide bash_process server for Isabelle/ML and other external programs;
clarified signature for Bash.params; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
proper prover_options for batch-build; — wenzelm / hgweb
clarified signature;
clarified errors; — wenzelm / hgweb
clarified signature: more options for bash_process; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
follow phabricator 2021 Week 26;
follow arcanist 2021 Week 23; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
unused; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
type classes for XML data representation; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified types: prefer Isabelle byte strings; — wenzelm / hgweb
merged — desharna / hgweb
added option labels to Mirabelle actions — desharna / hgweb
more operations: dest binders; — wenzelm / hgweb
clarified abstract and concrete boolean algebras — haftmann / hgweb
antiquotation for bundles — haftmann / hgweb
prefer persistent hash code for cachable items (see also 72b13af7f266); — wenzelm / hgweb
merged — wenzelm / hgweb
more operations: record overall exported entities; — wenzelm / hgweb
merged — desharna / hgweb
added dummy_fof prover to Sledgehammer — desharna / hgweb
fixed malconfigured option output_dir in mirabelle — desharna / hgweb
merged — wenzelm / hgweb
clarified export of formal entities: name space info is always present, but content depends on option "export_theory"; — wenzelm / hgweb
proper name space "kind": this is a formal name, not comment; — wenzelm / hgweb
more uniform signatures in ML and Scala; — wenzelm / hgweb
merged — desharna / hgweb
fixed typo — desharna / hgweb
added dummy_thf prover to Sledgehammer — desharna / hgweb
simplified hierarchy of type classes for bit operations — haftmann / hgweb
obsolete — haftmann / hgweb
more operations, notably free and bound variables as in Isabelle/Pure; — wenzelm / hgweb
more operations on types and terms;
abstract syntax operations for Pure and HOL; — wenzelm / hgweb
clarified jEdit java sources; — wenzelm / hgweb
clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons; — wenzelm / hgweb
removed junk; — wenzelm / hgweb
moved theory Bit_Operations into Main corpus — haftmann / hgweb
more operations; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
organize syntax for word operations in bundles — haftmann / hgweb
support for Lazy.Text; — wenzelm / hgweb
prefer compact Isabelle.Bytes; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature --- more operations; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified order of modules; — wenzelm / hgweb
more operations; — wenzelm / hgweb
tuned; — wenzelm / hgweb

#65 (Aug 15, 2021, 12:14:00 AM)

metadata update for MFMC_Countable — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
derive rel_pmf characterization from bounded and unbounded MFMC theorem — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
drop boundedness requirement for the sink — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
avoid global tmp file: pointless due to implicit theory export; — wenzelm / hgweb
repaired syntax — haftmann / hgweb
tuned signature, following Isabelle/d030b988d470; — wenzelm / hgweb
generalized gt_rat_sign_change to square-free polynomials — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
minor updates to bibliography — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
clarified signature; — wenzelm / hgweb
clarified abstract and concrete boolean algebras — haftmann / hgweb
antiquotation for bundles — haftmann / hgweb
simplified hierarchy of type classes for bit operations — haftmann / hgweb
restored executable conversions — haftmann / hgweb
dropped junk — haftmann / hgweb
moved theory Bit_Operations into Main corpus — haftmann / hgweb
organize syntax for word operations in bundles — haftmann / hgweb
more systematic approach for instantiation — haftmann / hgweb
avoid seemingly unused transfer rules — haftmann / hgweb

#63 (Aug 1, 2021, 12:14:00 AM)

clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
merged — wenzelm / hgweb
prefer Isabelle.Bytes, based on ShortByteString; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned signature: more generic operations; — wenzelm / hgweb
prefer UTF8 implementation from Data.Text.Encoding (foreign C);
clarified signatures and modules; — wenzelm / hgweb
documented Mirabelle_Sledgehammer's new keep semantics — desharna / hgweb
changed Mirabelle_Sledgehammer keep option from path to boolean — desharna / hgweb
added automatic uniform stride option to Mirabelle — desharna / hgweb
fixed HOL-ex following a5bab59d580b — desharna / hgweb
added support for TFX $let to Sledgehammer's TPTP output — desharna / hgweb
merged — desharna / hgweb
fixed TFX generation when universal quantifier is used as term — desharna / hgweb
merged — wenzelm / hgweb
various improvements of "isabelle scala_project"; — wenzelm / hgweb
support for native symlinks on Windows; — wenzelm / hgweb
tuned Mirabelle's theory selection — desharna / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
updated for Isabelle2021 release; — wenzelm / hgweb
back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012 R2); — wenzelm / hgweb
update to Haskell stack-2.7.3 and stackage lts-17.15; — wenzelm / hgweb
clarified version: Apple now counts like 11, 12, ...; — wenzelm / hgweb

#63 (Aug 1, 2021, 12:14:00 AM)

cleaner presentation of analysis theorems in preliminaries — yonoteam / hgweb
Update to new Epistemic_Logic.thy — Asta Halkjær From <andro.from@gmail.com> / hgweb
Avoid typedefs — Asta Halkjær From <andro.from@gmail.com> / hgweb
Clean: set AFP standard document options — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Clean: re-add to chapter AFP — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Finitely_Generated_Abelian_Groups website — paulson <lp15@cam.ac.uk> / hgweb
new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
Added Finitely_Generated_Abelian_Groups to metadata — Manuel Eberl <eberlm@in.tum.de> / hgweb

#62 (Jul 25, 2021, 12:14:00 AM)

clarified signature; — wenzelm / hgweb
clarified compiler output: allow multithreaded execution; — wenzelm / hgweb
clarified signature: more operations; — wenzelm / hgweb
clarified props: more permissive; — wenzelm / hgweb
more robust; — wenzelm / hgweb
clarified properties: "module" and "no_build";
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
tuned document; — wenzelm / hgweb
clarified names (again), e.g. relevant for "Plugin Options"; — wenzelm / hgweb
added simp_options to meson — desharna / hgweb
tuning — blanchet / hgweb
parse TPTP operator @ also when not parenthesized — blanchet / hgweb
removed setup for outdated CVC3 from Isabelle — blanchet / hgweb
tuned E's lambda encoding — blanchet / hgweb
use Vampire's clausifier with iProver, now that E's is no longer supported — blanchet / hgweb
updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain — blanchet / hgweb
compile — blanchet / hgweb
tuned; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
updated documentation on Isabelle/Scala; — wenzelm / hgweb
discontinued obsolete Apple (deprecated); — wenzelm / hgweb
clarified component setup: exclude jar from active component, but use sources from template within ISABELLE_HOME (relevant for "isabelle scala_project -L"); — wenzelm / hgweb
more robust "isabelle build_scala" as separate tool; — wenzelm / hgweb
tuned --- based on hints by IntelliJ IDEA; — wenzelm / hgweb
more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0); — wenzelm / hgweb
more portable across history; — wenzelm / hgweb
proper isabelle.setup.Setup build; — wenzelm / hgweb
rebuild component; — wenzelm / hgweb
more complete scala_project, including Isabelle/jEdit plugins; — wenzelm / hgweb
clarified directories; — wenzelm / hgweb
more accurate scala_project, based on build.props of components; — wenzelm / hgweb
clarified build_props: empty module means no build;
clarified signature;
clarified errors; — wenzelm / hgweb
tuned; — wenzelm / hgweb
CONTRIBUTORS — haftmann / hgweb
merged — wenzelm / hgweb
more robust; — wenzelm / hgweb
rebuild component; — wenzelm / hgweb
more robust: for the sake of Isabelle.app on macOS; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more robust; — wenzelm / hgweb
rebuild component; — wenzelm / hgweb
more informative errors: capture low-level compiler output; — wenzelm / hgweb
more direct isabelle_scala_build: always enabled, no "Admin" requirement; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
clarified names; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
clarified directory; — wenzelm / hgweb
clarified names; — wenzelm / hgweb
clarified component setup for old graph browser; — wenzelm / hgweb
redundant: *.class and *.jar are already ignored; — wenzelm / hgweb
proper cat_lines: avoid last "\n"; — wenzelm / hgweb
merged — paulson / hgweb
A few new lemmas and simplifications — paulson <lp15@cam.ac.uk> / hgweb
removed support for experimental Pirate prover — blanchet / hgweb

#62 (Jul 25, 2021, 12:14:00 AM)

Sync with my development repo. Add new material: "concrete bicategories" and
"bicategory of categories". Change sublocale declarations related to
functor/natural transformation/natural isomorphism to avoid issues with
global interpretations reported by Filip Smola, 2/2/2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb

#61 (Jul 18, 2021, 12:14:00 AM)

get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options — blanchet / hgweb
merged — wenzelm / hgweb
NEWS; — wenzelm / hgweb
proper example; — wenzelm / hgweb
more tests; — wenzelm / hgweb
more robust: component might be absent; — wenzelm / hgweb
clarified global state: allow to deactivate main plugin; — wenzelm / hgweb
more robust (again): allow to deactivate main plugin; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more complete dockables; — wenzelm / hgweb
more robust (see 4d91b6d5d49c); — wenzelm / hgweb
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin; — wenzelm / hgweb
more robust; — wenzelm / hgweb
tuned; — wenzelm / hgweb
avoid non-standard encoding; — wenzelm / hgweb
proper cross-platform build: jdk component is required for ISABELLE_SETUP_CLASSPATH in other_isabelle; — wenzelm / hgweb
more robust classpath: skip empty entries; — wenzelm / hgweb
more robust: avoid duplicate classpath entries; — wenzelm / hgweb
build.props for isabelle.jar, including isabelle.jedit;
build minimal Isabelle/jEdit plugins on the spot;
regular "jedit" component: discontinued special "jedit_build";
Isabelle/Scala services via jars, instead of settings; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more portable: avoid Windows CRLF in classpath output; — wenzelm / hgweb
proper lines (amending 59b6f0462086); — wenzelm / hgweb
more systematic treatment of encodings; — wenzelm / hgweb
tuned; — wenzelm / hgweb
extended the 'corec' format slightly — blanchet / hgweb
prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent — blanchet / hgweb
tuning — blanchet / hgweb
rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option — blanchet / hgweb
correctly translate constructor argument in 'primrec' — blanchet / hgweb
simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
revisited ac28714b7478: more faithful preplaying with chained facts — blanchet / hgweb
wait for E 2.7 before using 'ite' in HO mode — blanchet / hgweb
added alternative E binary name — blanchet / hgweb
parse logical operators in the right order w.r.t. backtracking — blanchet / hgweb
improved warning — blanchet / hgweb
adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing) — blanchet / hgweb
operations for symbolic computation of bit operations — haftmann / hgweb
proper local context — haftmann / hgweb
shasum for project meta-info; — wenzelm / hgweb
even more strict shasum (amending c9771e1b3223); — wenzelm / hgweb
clarified Isabelle meta-info within jar; — wenzelm / hgweb
strict shasum: this is used on input files; — wenzelm / hgweb
clarified modules;
clarified messages;
clarified return code; — wenzelm / hgweb
support for command-line operations; — wenzelm / hgweb
operations for all components; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
merged — wenzelm / hgweb
rebuild component; — wenzelm / hgweb
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER; — wenzelm / hgweb
support expand_platform_path, which is reminiscent of isabelle.Path.expand; — wenzelm / hgweb
skip scalac for Java build; — wenzelm / hgweb
support mixed Scala/Java build;
clarified scalac/javac options; — wenzelm / hgweb
clarified javac options; — wenzelm / hgweb
clarified syntax: similar to URL; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more compiler_deps via "requirements", notably jar list from settings;
proper Files.createDirectories; — wenzelm / hgweb
clarified component settings; — wenzelm / hgweb
clarified shasum: sources / resources within jar; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
merged — desharna / hgweb
fixed HOL-TPTP following f58108b7a60c — desharna / hgweb
documented Sledgehammer option "induction_rules" — desharna / hgweb
refactored Sledgehammer option "induction_rules" — desharna / hgweb
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules" — desharna / hgweb
jenkins: add pre/post-hook results for benchmark — Fabian Huch <huch@in.tum.de> / hgweb
remove SpecCheck; it is now part of the AFP — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb

#61 (Jul 18, 2021, 12:14:00 AM)

compile — blanchet / hgweb
more realistic timeout: 50min CPU time; — wenzelm / hgweb
Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending
on Finitely_Generated_Abelian_Groups — Joseph Thommes <joseph-thommes@gmx.de> / hgweb
new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
remove duplicate entry in metadata — Lars Hupel <lars.hupel@mytum.de> / hgweb
more coherent dependencies — haftmann / hgweb
fix(Regex_Equivalence) update to new SpecCheck version — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
operations for symbolic computation of bit operations — haftmann / hgweb
fixed Proof_Strategy_Language following Isabelle/f58108b7a60c — desharna / hgweb
SpecCheck now without _ (Regex_Equivalence is still broken) — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#60 (Jul 11, 2021, 12:14:00 AM)

merged — desharna / hgweb
added documentation for changes to Sledgehammer option "lam_trans" — desharna / hgweb
jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
merged — desharna / hgweb
added opaque_combs and renamed hide_lams to opaque_lifting — desharna / hgweb
more robust treatment of empty string; — wenzelm / hgweb
invoke Scala compiler from Java, without external process;
tuned messages; — wenzelm / hgweb
clarified version: Apple now counts like 11, 12, ...; — wenzelm / hgweb
Imported lots of material from Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb

#60 (Jul 11, 2021, 12:14:00 AM)

T1 fontenc for new entries — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
update hide_lams -> opaque_lifting — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
merged from afp2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
website for SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
metadata and sitegen for MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sitegen for Public Announcement Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry "Public Announcement Logic"
(and sorted ROOTS + removed duplicate entries in ROOTS) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
fixed a messy reference — paulson <lp15@cam.ac.uk> / hgweb
Van_der_Waerden website — paulson <lp15@cam.ac.uk> / hgweb
new entry Van_der_Waerden — paulson <lp15@cam.ac.uk> / hgweb
New entry IMP_Compiler — nipkow / hgweb
Removal of unintended files — Susannah Mansky <susannahej@gmail.com> / hgweb
Hidden.thy to Isar — Susannah Mansky <susannahej@gmail.com> / hgweb
merged — desharna / hgweb
renamed hide_lams opaque_lifting — desharna / hgweb
merged — Fabian Huch <huch@in.tum.de> / hgweb
jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
changed to opaque_lifiting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
Added missing Public_Announcement_Logic to ROOTS file — Manuel Eberl <eberlm@in.tum.de> / hgweb
More Support on Clean Syntax, Basic Lens Support, New Examples. — Burkhart Wolff <wolff@lri.fr> / hgweb
finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb

#59 (Jul 4, 2021, 12:14:00 AM)

merged — paulson / hgweb
arg for the nonstandard complex numbers — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
converting arg to Arg — paulson <lp15@cam.ac.uk> / hgweb
just a bit of tidying up — paulson <lp15@cam.ac.uk> / hgweb
create jar in pure Java; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified order; — wenzelm / hgweb
proper treatment of leading zero; — wenzelm / hgweb
support for jar resources; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
support for Isabelle/Scala in pure Java; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified directories; — wenzelm / hgweb
clarified modules and signatures; — wenzelm / hgweb
back to scala-2.13.5: avoid problems with history in scala REPL; — wenzelm / hgweb
tuned imports; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified Isabelle/Java/Scala project setup; — wenzelm / hgweb
support for Isabelle setup in pure Java; — wenzelm / hgweb
tuned: prefer Java interfaces; — wenzelm / hgweb
clarified package: towards stand-alone setup; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more direct java.home, according to current jdk directory layout; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules;
avoid initial use of _settings during init; — wenzelm / hgweb
tuned: prefer Java interfaces; — wenzelm / hgweb
tuned: prefer Java interfaces; — wenzelm / hgweb
clarified signature: prefer Java interfaces; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
proper usage; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules (again): services require full Isabelle/Scala environment; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
updated to scala-2.13.6, with scala-xml 1.3.0 ~> 2.0.0; — wenzelm / hgweb
clarified environment (amending 9444489766a1); — wenzelm / hgweb
merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
move code setup from Cardinality to separate theory — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
A few useful lemmas about derivatives, colinearity and other topics — paulson <lp15@cam.ac.uk> / hgweb

#59 (Jul 4, 2021, 12:14:00 AM)

arg -> Arg: the last holdout — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
arg -> Arg — paulson <lp15@cam.ac.uk> / hgweb
Add entry public announcement logic — Asta Halkjær From <andro.from@gmail.com> / hgweb
merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
adapt to changes in HOL-Library.Cardinality — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
Added Approximation_Algorithm for Center_Selection — nipkow / hgweb

#58 (Jun 27, 2021, 12:14:00 AM)

proper Font_Subst.cache for paintScreenLineRange; — wenzelm / hgweb
more predictable result, avoid slightly odd "lastSubstFont" by jEdit; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
discontinue i21of4 (old Apple hardware); — wenzelm / hgweb
avoid deprecated operation; — wenzelm / hgweb
tuned; — wenzelm / hgweb
support for jEdit font substitution; — wenzelm / hgweb
more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
more direct TextAttribute.RUN_DIRECTION_LTR (see also ce22e5c3d4ce); — wenzelm / hgweb
updated to flatlaf-1.2; — wenzelm / hgweb
proper directories after reinstallation of lxbroy10; — wenzelm / hgweb
more visual emphasis on node status; — wenzelm / hgweb
more word cleanup — haftmann / hgweb
merged — haftmann / hgweb
more default simp rules — haftmann / hgweb
some word streamlining — haftmann / hgweb
avoid legacy domain informatik.tu-muenchen.de; — wenzelm / hgweb

#58 (Jun 27, 2021, 12:14:00 AM)

proved conditional completeness of compilation — desharna / hgweb
fixed typos — nipkow / hgweb
more word cleanup — haftmann / hgweb
more default simp rules — haftmann / hgweb
some word streamlining — haftmann / hgweb
made consistent again — haftmann / hgweb
Fixed entry name for theories in sub-directory — Fabian Huch <huch@in.tum.de> / hgweb
Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb

#57 (Jun 20, 2021, 12:14:00 AM)

tuned --- following hints by IntelliJ; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature (see 2d6a489adb01); — wenzelm / hgweb
added support for TFX's and THF's $ite to Sledgehammer — desharna / hgweb
tuned Mirabelle documentation — desharna / hgweb
shortened long lines — desharna / hgweb
fixed typos — desharna / hgweb
updated Mirabelle documentation — desharna / hgweb
changed Mirabelle's filter to use short theory names — desharna / hgweb
more lemmas — haftmann / hgweb

#57 (Jun 20, 2021, 12:14:00 AM)

Relational_Disjoint_Set_Forests: updated metadata to reflect added theory — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
lemma grooming — haftmann / hgweb
no duplicates of shift operations — haftmann / hgweb
merge Jinja/Isar work — Gerwin Klein <kleing@unsw.edu.au> / hgweb
updated change history for Interpreter_Optimization — desharna / hgweb
merged — paulson / hgweb
updated, replacing axiomatizations by proper locales — paulson <lp15@cam.ac.uk> / hgweb
added basic blocks — desharna / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Merge from default, esp JinjaDCI — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb

#56 (Jun 13, 2021, 12:14:59 AM)

added support for unbounded max calls to Mirabelle — desharna / hgweb
added warnings when defining unamed or redefining Mirabelle action — desharna / hgweb
tuned whitespace; — wenzelm / hgweb
tuned Mirabelle — desharna / hgweb
merged — desharna / hgweb
refactored Mirabelle to produce output in real time — desharna / hgweb
global interpretation into nested targets — haftmann / hgweb
more succint interfaces — haftmann / hgweb
merged — wenzelm / hgweb
tuned messages; — wenzelm / hgweb
NEWS; — wenzelm / hgweb
proper profiling within command execution: messages require PIDE id; — wenzelm / hgweb
more systematic treatment of profiling mode; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
prefer less intrusive tracing message; — wenzelm / hgweb
clarified documentation: tracing messages are not shown here; — wenzelm / hgweb
add missing file; — wenzelm / hgweb
more formal ML profiling messages; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
Lukas Steven's more general fold foctions for maps — nipkow / hgweb
More general fold function for maps — nipkow / hgweb
follow Phabricator update 2021 Week 23; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more formal theory and session names;
tuned whitespace; — wenzelm / hgweb
proper NEWS after Isabelle2021; — wenzelm / hgweb
updated descriptions; — wenzelm / hgweb
allow system option short form NAME for NAME=true for type string, not just bool;
support short system options "-o document" and "-o system_log"; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more robust within session "HOL"; — wenzelm / hgweb
merged — wenzelm / hgweb
suppress theories from other sessions, unless explicitly specified via mirabelle_theories; — wenzelm / hgweb
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT); — wenzelm / hgweb
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more uniform schedule_theories, notably for "present" and "commit" phase after loading; — wenzelm / hgweb
tuned; — wenzelm / hgweb
moved more legacy to AFP — haftmann / hgweb

#56 (Jun 13, 2021, 12:14:59 AM)

Fix typo in date — Asta Halkjær From <andro.from@gmail.com> / hgweb
Lukas Steven's changes for his fold updates — nipkow / hgweb
moved more legacy to AFP — haftmann / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
suppress site-gen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
exclude etc/ in afp_check_roots — Gerwin Klein <kleing@unsw.edu.au> / hgweb
strip trailing whitespace; make full URL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
update usage instrucions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
more robust component setup for AFP/thys: support "isabelle components -u" and init $AFP_BASE on demand;
no ROOTS in $AFP_BASE: proper support for "isabelle build -a" with $AFP_BASE component, but without $AFP component; — wenzelm / hgweb
sitegen for Lifting_the_Exponent — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Lifting_the_Exponent — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#55 (Jun 6, 2021, 12:14:00 AM)

clarified modules; — wenzelm / hgweb
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys); — wenzelm / hgweb
tuned; — wenzelm / hgweb
more thorough update of required files (amending 1529c3eb6bac); — wenzelm / hgweb
clarified examples; — wenzelm / hgweb
tuned proofs; — wenzelm / hgweb
misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); — wenzelm / hgweb
tuned --- reduced source complexity; — wenzelm / hgweb
proper usage (amending f7ea394490f5); — wenzelm / hgweb
merged, resolving minor conflict; — wenzelm / hgweb
allow build session setup, e.g. for protocol handlers; — wenzelm / hgweb
unused; — wenzelm / hgweb
tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated); — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
removed pointless option (see 3d0952893db8); — wenzelm / hgweb
tuned --- avoid redundant future tasks from already loaded theories; — wenzelm / hgweb
no comment --- topological order appears to be fine since 04-Mar-2013; — wenzelm / hgweb
more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7); — wenzelm / hgweb
moved stride option from sledgehammer action to main mirabelle — desharna / hgweb
merged — paulson / hgweb
new lemmas mostly about paths — paulson <lp15@cam.ac.uk> / hgweb
lexorders the locale way — haftmann / hgweb
more accurate export morphism enables proper instantiation by interpretation — haftmann / hgweb

#55 (Jun 6, 2021, 12:14:00 AM)

more specific export_files: omit recent additions ("document", "PIDE", etc.); — wenzelm / hgweb
grouped lemmas — haftmann / hgweb
bundles for traditional infix syntax — haftmann / hgweb

#54 (May 30, 2021, 12:14:00 AM)

merged — paulson / hgweb
some new and/or varient results about images — paulson <lp15@cam.ac.uk> / hgweb
nicer statement of Liouville_theorem — paulson <lp15@cam.ac.uk> / hgweb
more lemmas — haftmann / hgweb
max word moved to Word_Lib in AFP — haftmann / hgweb
more robust syntax; — wenzelm / hgweb
unused; — wenzelm / hgweb
clarified document export names; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac; — wenzelm / hgweb
compose Latex text as XML, output exported YXML in Isabelle/Scala; — wenzelm / hgweb
more direct index_entry: no positions required -- text is eventually moved to .ind file; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle"); — wenzelm / hgweb
tuned message, e.g. for Pure bootstrap; — wenzelm / hgweb
proper signature export (amending b50f8cc8c08e); — wenzelm / hgweb
syslog option for "isabelle build"; — wenzelm / hgweb
further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea); — wenzelm / hgweb
merged — wenzelm / hgweb
NEWS; — wenzelm / hgweb
clarified index, more like formal @{element_ref}; — wenzelm / hgweb
clarified treatment of type constructors; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified context; — wenzelm / hgweb
more uniform document antiquotations for ML: consolidate former setup for manuals; — wenzelm / hgweb
clarified names; — wenzelm / hgweb
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature: avoid dispatch via name; — wenzelm / hgweb
clarified, e.g. type variables; — wenzelm / hgweb
tuned index; — wenzelm / hgweb
more ambitious default for index "is like"; — wenzelm / hgweb
tuned; — wenzelm / hgweb
support for index entries; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
clarified old document build; — wenzelm / hgweb
unused; — wenzelm / hgweb
prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee; — wenzelm / hgweb
prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document; — wenzelm / hgweb
unused; — wenzelm / hgweb
proper Unix lines; — wenzelm / hgweb
prefer explicit option document_bibliography (actually ignored by build script); — wenzelm / hgweb
explicit option document_bibliography; — wenzelm / hgweb
proper bibliography; — wenzelm / hgweb
discontinued obsolete "isabelle latex"; — wenzelm / hgweb
more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
clarified ISABELLE_MAKEINDEX options; — wenzelm / hgweb
default document_build (lualatex); — wenzelm / hgweb
more robust: allow \printindex within the document; — wenzelm / hgweb
clarified bash scripts, with public interfaces for user-defined Document_Build.Engine; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
option document_preprocessor; — wenzelm / hgweb
show symbols in Isabelle/ML instead of perl; — wenzelm / hgweb
more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; — wenzelm / hgweb
tuned --- more robust; — wenzelm / hgweb
discontinued somewhat pointless "fixbookmarks": default output works sufficiently well; — wenzelm / hgweb
more uniform bibtex error, without using perl (see 4710dd5093a3); — wenzelm / hgweb
proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error); — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified command-line options; — wenzelm / hgweb
obsolete (see 5a3a2a52648d); — wenzelm / hgweb
redundant: copy produced from session document_files; — wenzelm / hgweb
clarified treatment of Isabelle .sty files; — wenzelm / hgweb
option document_logo; — wenzelm / hgweb
proper options; — wenzelm / hgweb
option document_build refers to build engine in Isabelle/Scala;
pdflatex is back as legacy build engine, e.g. for published proceedings; — wenzelm / hgweb
redundant: tmp_dir is purged anyway; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
tuned --- clarified corner cases; — wenzelm / hgweb
more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases; — wenzelm / hgweb
clarified signature -- avoid odd warning about scala/bug#6675; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
proper syntax of Scala 3; — wenzelm / hgweb
enforce syntax of Scala 3; — wenzelm / hgweb

#54 (May 30, 2021, 12:14:00 AM)

complement reduced to mere abbreviation — haftmann / hgweb
extracted more legacy abbreviations — haftmann / hgweb
max word moved to Word_Lib in AFP — haftmann / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
update website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
fix links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Restore deleted theorem from Szpilrajn — Lukas Stevens <mail@lukas-stevens.de> / hgweb
tuned presentation — haftmann / hgweb
adapted to devel — nipkow / hgweb
adjusted to changes in distribution — haftmann / hgweb
adjust Combinatorics_Words to isabelle@493b1ae188da — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
make AFP ROOTS globally available for component — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merged — nipkow / hgweb
New entries Combinatorics_Words* — nipkow / hgweb
adjusted to change in distribution — haftmann / hgweb
adapted to Isabelle/466fae6bf22e; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
Remove comment about missing refinement — n.muendler <n.muendler@tum.de> / hgweb
continued uglification, but also fixed some dodgy proofs — paulson <lp15@cam.ac.uk> / hgweb
fixed some broken / looping / fragile proofs — paulson <lp15@cam.ac.uk> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
simplify usage instructions more — Gerwin Klein <kleing@unsw.edu.au> / hgweb
sitegen for Padic_Ints — Manuel Eberl <eberlm@in.tum.de> / hgweb
new entry: Padic_Ints — Manuel Eberl <eberlm@in.tum.de> / hgweb
update affiliation — Gerwin Klein <kleing@unsw.edu.au> / hgweb
New entry: Regressioon_Test_Selection — nipkow / hgweb
metadata for Metalogic_ProofChecker — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Metalogic_ProofChecker — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
metadata for GaleStewart_Games — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry GaleStewart_Games — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
fixed the ROOT file ofr BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
webpage for BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
new entry BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
Slight tidying to shorten too-long lines — paulson <lp15@cam.ac.uk> / hgweb
added a necessary acknowledgment (ERC) — paulson <lp15@cam.ac.uk> / hgweb
New entry Progress_Tracking — nipkow / hgweb
Revisions by Wenda to eliminate the locale comp_affine_scheme — paulson <lp15@cam.ac.uk> / hgweb
renamed a lemma — paulson <lp15@cam.ac.uk> / hgweb
Fixed an error in the statement of closed_subsets_empty. Also added syntax priority hints for carrier_of_local_ring_at. — paulson <lp15@cam.ac.uk> / hgweb
consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry: Grothendieck_Schemes — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
metadata for IFC_Tracking — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry IFC_Tracking — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
merged — wenzelm / hgweb
adapted to Isabelle/ef1a18e20ace; — wenzelm / hgweb
recover some patches after years of continuously changing Isabelle LaTeX output; — wenzelm / hgweb
prefer document_preprocessor over document_build; — wenzelm / hgweb
prefer document_logo instead of document_build script; — wenzelm / hgweb
proper options; — wenzelm / hgweb

#53 (May 23, 2021, 12:14:00 AM)

things need to be ugly — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
sorted as an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
mere abbreviation for logical alias — haftmann / hgweb
avoid unexpected output+behaviour when CDPATH is set — kleing / hgweb
recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04); — wenzelm / hgweb
avoid perl; — wenzelm / hgweb
tuned signature --- following hints by IntelliJ IDEA; — wenzelm / hgweb
ignore session build timeout, notably in AFP; — wenzelm / hgweb
check timeout_ignored as in ML, before applying timeout_scale; — wenzelm / hgweb
merged — wenzelm / hgweb
proper build of required session images vs. build with Mirabelle presentation; — wenzelm / hgweb
reactive "sledgehammer"; — wenzelm / hgweb
reactive "sledgehammer_filter": statically correct, but untested (no proof_file); — wenzelm / hgweb
clarified command-line; — wenzelm / hgweb
clarified signature;
supporess empty results; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified log content; — wenzelm / hgweb
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; — wenzelm / hgweb
tuned; — wenzelm / hgweb
unused; — wenzelm / hgweb
unused (see 8ffc607c345d); — wenzelm / hgweb
clarified signature: provide access to previous state; — wenzelm / hgweb
clarified signature (see Scala version); — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
avoid duplicate loading of ML file; — wenzelm / hgweb

#53 (May 23, 2021, 12:14:00 AM)

PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of "properties" — paulson <lp15@cam.ac.uk> / hgweb
fixed two more "sorted" errors — paulson <lp15@cam.ac.uk> / hgweb
fixed two "sorted" issues — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
changes for "sorted" as an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
mere abbreviation for logical alias — haftmann / hgweb
eliminated odd clone (see Isabelle/caa5a257d3ed); — wenzelm / hgweb

#52 (May 16, 2021, 12:14:00 AM)

strict_sorted now an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
explicit type class operations for type-specific implementations — haftmann / hgweb
obsolete — haftmann / hgweb
added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran — desharna / hgweb
merged — nipkow / hgweb
generalized type — nipkow / hgweb
basic setup of Isabelle setup tool --- pure Java, no dependencies; — wenzelm / hgweb
merged — wenzelm / hgweb
guess package more directly; — wenzelm / hgweb
merged — paulson / hgweb
Just one lemma — paulson <lp15@cam.ac.uk> / hgweb
proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64; — wenzelm / hgweb
clarified platforms; — wenzelm / hgweb
merged — wenzelm / hgweb
proper jEdit.props (amending ff716ecb0805); — wenzelm / hgweb
update to gmp-6.2.1, with support for arm64-darwin; — wenzelm / hgweb
clarified platforms; — wenzelm / hgweb
clarified options: implicitly support both x86_64 and arm64; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
centralized more lemmas — haftmann / hgweb
avoid Fun.swap — haftmann / hgweb
guide is out of focus — haftmann / hgweb
proper build for fresh target directory (amending d9823224fcfe); — wenzelm / hgweb
put more resources into jedit_build component; — wenzelm / hgweb
more brackets (see f6b453449cc6); — wenzelm / hgweb
more brackets; — wenzelm / hgweb
proper settings variable, amending 6e85281177df; — wenzelm / hgweb
merged — wenzelm / hgweb
tuned proofs --- avoid z3, which is absent on arm64-linux; — wenzelm / hgweb
proper condition: z3 could be absent, e.g. on arm64-linux; — wenzelm / hgweb
build auxiliary jEdit component in Isabelle/Scala;
clarified directory layout; — wenzelm / hgweb
separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597); — wenzelm / hgweb
tuned message; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more elementary swap — haftmann / hgweb

#52 (May 16, 2021, 12:14:00 AM)

strict_sorted now an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
deleted needless material — paulson <lp15@cam.ac.uk> / hgweb
explicit type class operations for type-specific implementations — haftmann / hgweb
next step to phase out ancient numerals — haftmann / hgweb
more small simplifications — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
fixed some latex; tried the alternative definition of Ramsey — paulson <lp15@cam.ac.uk> / hgweb
Trying out Ramsey_eq for simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
more tiny tweaks — paulson <lp15@cam.ac.uk> / hgweb
centralized more lemmas — haftmann / hgweb
avoid Fun.swap — haftmann / hgweb
guide is out of focus — haftmann / hgweb
Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
more elementary swap — haftmann / hgweb

#49 (Apr 25, 2021, 12:14:00 AM)

collecting more lemmas concerning multisets — haftmann / hgweb

#49 (Apr 25, 2021, 12:14:00 AM)

collecting more lemmas concerning multisets — haftmann / hgweb

#47 (Apr 21, 2021, 10:29:10 AM)

proper use of antiquotations; — wenzelm / hgweb
more documentation on "Conversions"; — wenzelm / hgweb
tuned — nipkow / hgweb
updated example; — wenzelm / hgweb
clarified options (again); — wenzelm / hgweb
more options: update ISABELLE_IDENTIFIER; — wenzelm / hgweb
clarified conditional ML; — wenzelm / hgweb
support for conditional ML text; — wenzelm / hgweb
updated example; — wenzelm / hgweb
clarified options; — wenzelm / hgweb
proper context variable handling when stripping leadings quantifiers from test goals — haftmann / hgweb
proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); — wenzelm / hgweb
eliminated perl: prefer elementary GNU printenv; — wenzelm / hgweb
more robust bootstrap of components; — wenzelm / hgweb
more self-contained support for macOS; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
support for base64 via Isabelle/Scala/ML; — wenzelm / hgweb
compile; — wenzelm / hgweb
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence); — wenzelm / hgweb
clarified signature (again); — wenzelm / hgweb
merged — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
unused; — wenzelm / hgweb
unused; — wenzelm / hgweb
clarified signature: more structured arguments, notably for remote provers; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature: avoid tmp file; — wenzelm / hgweb
clarified signature for Scala functions; — wenzelm / hgweb
clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified cache; — wenzelm / hgweb
clarified signature: Bytes extends CharSequence already (see d201996f72a8); — wenzelm / hgweb
clarified exceptions; — wenzelm / hgweb
more uniform use of Byte_Message;
support protocol_message with multiple chunks; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more robust treatment of empty markup: it allows to produce formal chunks; — wenzelm / hgweb
collected combinatorial material — haftmann / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more documentation; — wenzelm / hgweb
proper treatment of nested antiquotations;
clarified signature; — wenzelm / hgweb
support for ML special forms: modified evaluation similar to Scheme; — wenzelm / hgweb
clarified signature: more detailed token positions for antiquotations; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
confluent preprocessing for floats in presence of target language numerals — haftmann / hgweb
subclass relation — haftmann / hgweb
some tinkering with npm versions; — wenzelm / hgweb
some tinkering with npm versions; — wenzelm / hgweb
back to post-release mode; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
auto-update due to "isabelle build_vscode"; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned --- following hints by IntelliJ IDEA; — wenzelm / hgweb
fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes) — Manuel Eberl <eberlm@in.tum.de> / hgweb
simplified definition — haftmann / hgweb
new lemmas — haftmann / hgweb
discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove"; — wenzelm / hgweb
following recent Phabricator update, after 2021 Week 13 (Late March); — wenzelm / hgweb
merged — paulson / hgweb
Cosmetic: no !! in the lemma statement — paulson <lp15@cam.ac.uk> / hgweb
clarified README;
avoid odd patching of sources; — wenzelm / hgweb
more standard header, with utf-8 encoding; — wenzelm / hgweb
clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources; — wenzelm / hgweb
merged — nipkow / hgweb
new automatic order prover: stateless, complete, verified — nipkow / hgweb
clarified signature; — wenzelm / hgweb
clarified: follow "isabelle version -t"; — wenzelm / hgweb
further clarification of Isabelle distribution identification -- avoid odd patching of sources; — wenzelm / hgweb
tuned signature -- more explicit types; — wenzelm / hgweb
more robust and uniform ISABELLE_TAGS; — wenzelm / hgweb
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos; — wenzelm / hgweb
simplified release status (again), in contrast to a43898f76ae9; — wenzelm / hgweb
more uniform HTTP resources; — wenzelm / hgweb
clarified (again): local tip could be actually more recent; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified name; — wenzelm / hgweb
more systematic java_library: avoid empty entries, declaration order as for other bash functions; — wenzelm / hgweb
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.; — wenzelm / hgweb
updated to latest latex due to new mechanism for dealing with bold ccfonts — nipkow / hgweb
removal of needless hypothesis in hd_rev and last_rev — paulson <lp15@cam.ac.uk> / hgweb

#47 (Apr 21, 2021, 10:29:10 AM)

more realistic timeout; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb
Tweaks — Asta Halkjær From <andro.from@gmail.com> / hgweb
adapted to Isabelle/a2c589d5e1e4; — wenzelm / hgweb
Merge — paulson <lp15@cam.ac.uk> / hgweb
tweak — paulson <lp15@cam.ac.uk> / hgweb
simplified proof — nipkow / hgweb
sshiftr/bl lemmas by Florian Märkl — Gerwin Klein <kleing@unsw.edu.au> / hgweb
proof simplification — paulson <lp15@cam.ac.uk> / hgweb
cosmetic tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
minor stylistic changes — paulson <lp15@cam.ac.uk> / hgweb
Add completeness of modal logics T, KB, K4, S4 and S5 — Asta Halkjær From <andro.from@gmail.com> / hgweb
Stylistic tweaks, which I hope are improvements :-) — paulson <lp15@cam.ac.uk> / hgweb
updated paper references — traytel / hgweb
merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
increased timeout — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
collected combinatorial material — haftmann / hgweb
Update root.tex — Asta Halkjær From <andro.from@gmail.com> / hgweb
Cut out Fitting's consistency properties — Asta Halkjær From <andro.from@gmail.com> / hgweb
fixed proof — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
clarified message, following Isabelle/a7aabdf889b7; — wenzelm / hgweb
confluent preprocessing for floats in presence of target language numerals — haftmann / hgweb
subclass relation — haftmann / hgweb
adapted to isabelle-dev/56db8559eadb — Manuel Eberl <eberlm@in.tum.de> / hgweb
simplified definition — haftmann / hgweb
new lemmas — haftmann / hgweb
probable fix suggested by Cornelius for the changes in the vicinity of 2cd23d587db9 — nipkow / hgweb
Fixes due to new order prover — nipkow / hgweb
another broken proof — paulson <lp15@cam.ac.uk> / hgweb
Fixed and simplified some failing proofs — paulson <lp15@cam.ac.uk> / hgweb
Writing less_sets as an infix — paulson <lp15@cam.ac.uk> / hgweb
avoid symblinks --- make it work on Windows; — wenzelm / hgweb
Fixed some looping proofs (though why they were looping isn't clear) — paulson <lp15@cam.ac.uk> / hgweb
Fixed a failing proof — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
fixes for new hd_rev and last_rev — paulson <lp15@cam.ac.uk> / hgweb

#42 (Apr 4, 2021, 12:14:00 AM)

more robust; — wenzelm / hgweb
clarified message; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
proper export; — wenzelm / hgweb
more options: build is part of default setup; — wenzelm / hgweb
misc tuning and clarification; — wenzelm / hgweb
more options; — wenzelm / hgweb
proper Admin script, outside the settings environment; — wenzelm / hgweb
tuned whitespace; — wenzelm / hgweb

#42 (Apr 4, 2021, 12:14:00 AM)

merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Infix notation for the less_sets relation — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
sitegen and metadata for Constructive_Cryptography_CM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
new entry Constructive_Cryptography_CM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb

#41 (Mar 28, 2021, 12:14:00 AM)

tuned; — wenzelm / hgweb
clarified; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
more accurate settings after update of current version; — wenzelm / hgweb
clarified messages; — wenzelm / hgweb
more robust: lest hg work out remote tip;
more options; — wenzelm / hgweb
more options; — wenzelm / hgweb
clarified treatment of multiple versions: last one counts;
more options; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more robust: explicit repository root; — wenzelm / hgweb
more robust; — wenzelm / hgweb
more convenient repository setup; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more robust invocation of hg; — wenzelm / hgweb
more robust: idempotent; — wenzelm / hgweb
more robust invocation of hg; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified output;
more options; — wenzelm / hgweb
support repository archives (without full .hg directory); — wenzelm / hgweb
more robust invocation of hg; — wenzelm / hgweb
record official releases that follow a certain structure, with public access via https://isabelle.sketis.net/repos/isabelle/raw-file/tip/Admin/Release/official (NB: Isabelle2013-1 had to be retracted); — wenzelm / hgweb
dedicated session for combinatorial material — haftmann / hgweb
support for Java Chromium Embedded Framework (JCEF): still somewhat fragile; — wenzelm / hgweb
enforce full build; — wenzelm / hgweb
turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont; — wenzelm / hgweb
discontinue fragile check in LaTeX, e.g. problems with toc entries; — wenzelm / hgweb
merged — paulson / hgweb
merged — paulson / hgweb
type class relaxation — paulson <lp15@cam.ac.uk> / hgweb
more NEWS; — wenzelm / hgweb
clarified group (but hard to tell); — wenzelm / hgweb
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
corresponding symbols and latex macros; — wenzelm / hgweb
more lemmas — haftmann / hgweb
clarified package name (actually both pxfonts and txfonts exist and have this font); — wenzelm / hgweb
tuned; — wenzelm / hgweb
prefer isabelle bbbfont; — wenzelm / hgweb
enforce full build; — wenzelm / hgweb
clarified symbol names, notably relevant for Z_Notation; — wenzelm / hgweb
update README (actually after update of component); — wenzelm / hgweb
high-quality blackboard-bold fonts from "txmia" (package "txfonts"); — wenzelm / hgweb

#41 (Mar 28, 2021, 12:14:00 AM)

more robust invocation of hg; — wenzelm / hgweb
Update tile to match metadata — Lukas Stevens <mail@lukas-stevens.de> / hgweb
Extend entry Szpilrajn — Lukas Stevens <mail@lukas-stevens.de> / hgweb
dedicated session for combinatorial material — haftmann / hgweb
more lemmas — haftmann / hgweb

#40 (Mar 21, 2021, 12:14:00 AM)

publish component; — wenzelm / hgweb
further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster; — wenzelm / hgweb
clarified \<Zcomp> (small) vs. \<Zsemi> (big); — wenzelm / hgweb
more CONTRIBUTORS; — wenzelm / hgweb
more Z_Notation symbols, as proposed by Simon Foster;
some LaTeX-art based on tex.stackexchange "How do you make a square element symbol (\in)"; — wenzelm / hgweb
more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus"; — wenzelm / hgweb
clarified order for GUI panel; — wenzelm / hgweb
prefer more direct interpretation — haftmann / hgweb
more Z_Notation symbols, as proposed by Simon Foster; — wenzelm / hgweb
more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt; — wenzelm / hgweb
clarified order for presentation in isar-ref (Appendix B); — wenzelm / hgweb
prefer explicit \<Zproject> (with its own Unicode codepoint); — wenzelm / hgweb
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
NB: no bold version of 0x2900 due to fontforge crash "Internal Error: Some fragments did not join"; — wenzelm / hgweb
tuned message; — wenzelm / hgweb
proper directory of settings file;
tuned; — wenzelm / hgweb
tuned lemma — nipkow / hgweb
added lemma — nipkow / hgweb
tuned signature; — wenzelm / hgweb
tuned signature (again); — wenzelm / hgweb
tuned --- following hints by IntelliJ; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
proper shell quote; — wenzelm / hgweb
removed spurious references to perl / libwww-perl; — wenzelm / hgweb
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
clarified inlined command-line;
clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function); — wenzelm / hgweb
clarified signature: refer to file name instead of file content; — wenzelm / hgweb
compile; — wenzelm / hgweb
clarified signature: more explicit types; — wenzelm / hgweb
support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
elapsed time to download content (and for the server to provide content); — wenzelm / hgweb
more direct elapsed run_time via bash_process wrapper (via Scala and C); — wenzelm / hgweb

#40 (Mar 21, 2021, 12:14:00 AM)

neater proof — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
Removal of an unused theorem. Plus lots of white space — paulson <lp15@cam.ac.uk> / hgweb
switch new entries' documents to T1 encoding — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
corrected metadata (use acute's in names of J. Divasón and René T.) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
sitegen for Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
metadata for Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
new entry Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
a slight streamlining — paulson <lp15@cam.ac.uk> / hgweb
Hermite_Lindemann website — paulson <lp15@cam.ac.uk> / hgweb
new entry Hermite_Lindemann — paulson <lp15@cam.ac.uk> / hgweb
cosmetic changes — paulson <lp15@cam.ac.uk> / hgweb
Projective_Measurements website — paulson <lp15@cam.ac.uk> / hgweb
Projective_Measurements with files — paulson <lp15@cam.ac.uk> / hgweb
new entry Projective_Measurements — paulson <lp15@cam.ac.uk> / hgweb
add Andreas Lochbihler as editor — Gerwin Klein <kleing@unsw.edu.au> / hgweb
New entry: Mereology — nipkow / hgweb
New entry Sunflowers — nipkow / hgweb
refactored and added lemma state_behaves_forward_to_backward — desharna / hgweb

#39 (Mar 14, 2021, 12:14:00 AM)

merged — wenzelm / hgweb
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages; — wenzelm / hgweb
clarified signature: let Sledgehammer handle SystemOnTPTP comments; — wenzelm / hgweb
clarified signature: url may change dynamically and is part of result; — wenzelm / hgweb
clarified error; — wenzelm / hgweb
support timeout, similar to perl LWP::UserAgent; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML; — wenzelm / hgweb
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); — wenzelm / hgweb
clarified HTTP.Content: support encoding;
more realistic HTTP.Client operations; — wenzelm / hgweb
clarified signature: more explicit HTTP operations; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more robust; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified components; — wenzelm / hgweb
avoid name clash — haftmann / hgweb
lemma — haftmann / hgweb
tuned; — wenzelm / hgweb
another example for lift_bnf for quotients — traytel / hgweb
merged — wenzelm / hgweb
proper \usepackage[T1]{fontenc}; — wenzelm / hgweb
more robust init: avoid spilling opam artifacts; — wenzelm / hgweb
proper type-setting of cartouches (requires T1);
\usepackage[T1]{fontenc} is default for mkroot;
\usepackage[utf8]{inputenc} is obsolete in lualatex; — wenzelm / hgweb
provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04; — wenzelm / hgweb
more robust;
eliminated perl; — wenzelm / hgweb
removed unused latex packages; — wenzelm / hgweb
obsolete (see 0c837beeb5e7); — wenzelm / hgweb
proper Isabelle/Scala tool --- avoid perl; — wenzelm / hgweb
generalized confluence-based subdistributivity theorem for quotients;
new example that triggered the generalization — traytel / hgweb
Backed out changeset 3fdb94d87e0e — desharna / hgweb
Backed out changeset b867b436f372 — desharna / hgweb
reduced dependencies on List_Permutation — haftmann / hgweb
follow corresponding precedence on sets — haftmann / hgweb
consolidated names — haftmann / hgweb
reduced dependencies on theory List_Permutation — haftmann / hgweb

#39 (Mar 14, 2021, 12:14:00 AM)

avoid name clash — haftmann / hgweb
adapted to LuaLaTeX according to Isabelle/299f6a8faccc;
\usepackage[T1]{fontenc} is default, it provides e.g. proper cartouche-delimiters;
\usepackage{lmodern} is no longer required, since T1 in LuaLaTeX has proper scalable fonts;
\usepackage[utf8]{inputenc} is obsolete in LuaLaTeX;
tuned whitespace; — wenzelm / hgweb
reduced dependencies on List_Permutation — haftmann / hgweb
follow corresponding precedence on sets — haftmann / hgweb
consolidated names — haftmann / hgweb
reduced dependencies on theory List_Permutation — haftmann / hgweb

#38 (Mar 7, 2021, 12:14:00 AM)

obsolete (see f3378101f555); — wenzelm / hgweb
merged — wenzelm / hgweb
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of input / digest; — wenzelm / hgweb
clarified smt: support Timeout.ignored and Timeout.scale_time; — wenzelm / hgweb
clarified timeouts in Isabelle/ML; — wenzelm / hgweb
tuned --- more elementary Time operations; — wenzelm / hgweb
removed unused/pointless operation: Time.start is the load/init time of this Scala module; — wenzelm / hgweb
obsolete; — wenzelm / hgweb
clarified signature --- augment existing structure Time; — wenzelm / hgweb
rebuild SMT certificates from scratch; — wenzelm / hgweb
added lemmas (sublist|prefix|suffix)_list_all — desharna / hgweb
added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While — desharna / hgweb
added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI — desharna / hgweb
typo — haftmann / hgweb
merged — desharna / hgweb
added upper bound on monomorphisation duplicate instances — desharna / hgweb
tuned best_slices in atp_config — desharna / hgweb
tuned exec field in atp_config — desharna / hgweb
removed junk; — wenzelm / hgweb
tuned proofs; — wenzelm / hgweb
enforce full build, after significant changes in Isabelle/Scala; — wenzelm / hgweb
clarified compiler options: show relevant warnings; — wenzelm / hgweb
tuned --- avoid compiler warnings; — wenzelm / hgweb
clarified signature --- fewer warnings; — wenzelm / hgweb
clarified signature --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
more robust ordering (see also 88c96e836ed6); — wenzelm / hgweb
proper scala.collection.immutable; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
more robust error; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
updated to scala-2.13.5 (with scala-swing_2.13-3.0.0); — wenzelm / hgweb
slightly more efficient Term.fastype_of (only little impact in regular applications); — wenzelm / hgweb
reduced dependencies on theory List_Permutation — haftmann / hgweb
Merge — paulson <lp15@cam.ac.uk> / hgweb
reverted simprule status on a new lemma — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
tiny bit of lemma hacking — paulson <lp15@cam.ac.uk> / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- avoid deprecated conversions between certain number type; — wenzelm / hgweb
tuned --- avoid deprecated Predef.any2stringadd; — wenzelm / hgweb
tuned --- silence odd warning; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
tuned --- fewer warnings; — wenzelm / hgweb
clarified signature, according to Isabelle/Scala; — wenzelm / hgweb
download more directly, via means of JVM; — wenzelm / hgweb
download on separate thread; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.); — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
NEWS — haftmann / hgweb
lemma diffusion — haftmann / hgweb
more connections between mset _ = mset _ and permutations — haftmann / hgweb
dissolve theory with duplicated name from afp — haftmann / hgweb
more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept; — wenzelm / hgweb
more Isabelle/ML/Scala operations; — wenzelm / hgweb
more Isabelle/ML/Scala operations; — wenzelm / hgweb
more Isabelle/ML/Scala operations;
clarified errors; — wenzelm / hgweb
proper src1, amending 20157c8ab3f3; — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper File.eq, amending df49ca5da9d0; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified modules: more like ML; — wenzelm / hgweb
obsolete; — wenzelm / hgweb
tuned; — wenzelm / hgweb
more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552); — wenzelm / hgweb
discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working; — wenzelm / hgweb

#38 (Mar 7, 2021, 12:14:00 AM)

tuned — nipkow / hgweb
Tuned presentation of Buffon's needle — Manuel Eberl <eberlm@in.tum.de> / hgweb
tuned — nipkow / hgweb
reduced dependencies on theory List_Permutation — haftmann / hgweb
tidied up messy proofs — paulson <lp15@cam.ac.uk> / hgweb
lemma diffusion — haftmann / hgweb
more connections between mset _ = mset _ and permutations — haftmann / hgweb
dissolve theory with duplicated name from afp — haftmann / hgweb

#37 (Feb 28, 2021, 12:14:00 AM)

more checks; — wenzelm / hgweb
clarified message; — wenzelm / hgweb
clarified message; — wenzelm / hgweb
clarified comments; — wenzelm / hgweb
clarified message; — wenzelm / hgweb
improved list_neq simproc — nipkow / hgweb
merged — haftmann / hgweb
repaired document — haftmann / hgweb
merged — paulson / hgweb
merged — paulson / hgweb
A couple of basic lemmas about arg — paulson <lp15@cam.ac.uk> / hgweb
multiset as equivalence class of permuted lists — haftmann / hgweb
emphasize connection to multisets — haftmann / hgweb
proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work; — wenzelm / hgweb
more on Isabelle_System.bash; — wenzelm / hgweb
more specific name — haftmann / hgweb
more lemmas — haftmann / hgweb
dropped obscure FIXME — haftmann / hgweb
proper usage of hypotheses for zipperposition's TPTP generation — desharna / hgweb
merged — desharna / hgweb
tuned Mirabelle to parse option check_trivial only once — desharna / hgweb
merged — desharna / hgweb
merged — desharna / hgweb
added stride option to Mirabelle — desharna / hgweb
proper prover capabilities for zipperposition — desharna / hgweb
NEWS; — wenzelm / hgweb
merged — wenzelm / hgweb
clarified uses of Isabelle_System.bash_process: more checks, fewer messages; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
more direct timing from bash_process wrapper; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature, following Isabelle/Scala; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code; — wenzelm / hgweb
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature, following Isabelle/Scala; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
clarified signature: process_result timing from Isabelle/Scala; — wenzelm / hgweb
NEWS — haftmann / hgweb
dedicated locale for preorder and abstract bdd operation — haftmann / hgweb
get rid of traditional predicate — haftmann / hgweb
proper treatment of process_result; — wenzelm / hgweb
more accurate process_result in ML, corresponding to Process_Result in Scala; — wenzelm / hgweb
clarified: proper trim_line for error; — wenzelm / hgweb
unused; — wenzelm / hgweb
clarified lines (again); — wenzelm / hgweb
clarified modules; — wenzelm / hgweb
more uniform Bash.process: always ask Isabelle/Scala; — wenzelm / hgweb
more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process); — wenzelm / hgweb
clarified compiler options; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
removed obsolete RC tags; — wenzelm / hgweb

#37 (Feb 28, 2021, 12:14:00 AM)

merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
revert accidental change — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
website update — Gerwin Klein <kleing@unsw.edu.au> / hgweb
fix typo (Bauer -> Bayer) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
new entry BTree — Gerwin Klein <kleing@unsw.edu.au> / hgweb
add Windows example to use-instructions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Isabelle app layout changed on Mac — Gerwin Klein <kleing@unsw.edu.au> / hgweb
Formal_Puiseux_Series website — paulson <lp15@cam.ac.uk> / hgweb
new entry Formal_Puiseux_Series — paulson <lp15@cam.ac.uk> / hgweb
2021 web pages — Gerwin Klein <kleing@unsw.edu.au> / hgweb
update with 2021 release .tar.gz's — Gerwin Klein <kleing@unsw.edu.au> / hgweb
add Isabelle2021 release date — Gerwin Klein <kleing@unsw.edu.au> / hgweb
update .tar.gz releases — Gerwin Klein <kleing@unsw.edu.au> / hgweb
set version to 2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
multiset as equivalence class of permuted lists — haftmann / hgweb
emphasize connection to multisets — haftmann / hgweb
more specific name — haftmann / hgweb
merged — wenzelm / hgweb
adapted to Isabelle/0110e2e2964c; — wenzelm / hgweb
adapted to Isabelle/f0db1e4c89bc; — wenzelm / hgweb
dedicated locale for preorder and abstract bdd operation — haftmann / hgweb
get rid of traditional predicate — haftmann / hgweb
more accurate process_result; — wenzelm / hgweb
adapted to Isabelle/440546ea20e6; — wenzelm / hgweb

#36 (Feb 21, 2021, 12:14:00 AM)

more hints; — wenzelm / hgweb
merged — wenzelm / hgweb
Added tag Isabelle2021 for changeset 7e2a9a8c2b85 — wenzelm / hgweb
provide naproche-755224402e36; — wenzelm / hgweb
provide naproche-4ad61140062f; — wenzelm / hgweb
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc. — Manuel Eberl <eberlm@in.tum.de> / hgweb
tidied up a few ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
merged — wenzelm / hgweb
provide naproche-6d0d76ce2f2a; — wenzelm / hgweb
Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b — wenzelm / hgweb
updated to flatlaf-1.0; — wenzelm / hgweb
tuned NEWS; — wenzelm / hgweb
tuned comments; — wenzelm / hgweb
more robust interrupt handling as in Future.forked_results (amending 64df1e514005); — wenzelm / hgweb
more parallelism: avoid exhaustion of standard thread pool; — wenzelm / hgweb

#36 (Feb 21, 2021, 12:14:00 AM)

follow_on changes from Complex_Geometry — paulson <lp15@cam.ac.uk> / hgweb
merged — paulson / hgweb
a massive simplification, thanks to sledgehammer, etc. — paulson <lp15@cam.ac.uk> / hgweb
adapted to isabelle-dev/73253:f6bb31879698 — Manuel Eberl <eberlm@in.tum.de> / hgweb
Buffons_Needle: tuned presentation — Manuel Eberl <eberlm@in.tum.de> / hgweb
Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is called 'vimage_algebra'. — Manuel Eberl <eberlm@in.tum.de> / hgweb

#34 (Feb 7, 2021, 12:14:00 AM)

merged — wenzelm / hgweb
updated for release; — wenzelm / hgweb
Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb — wenzelm / hgweb
provide naproche-20210201; — wenzelm / hgweb
clarified messages; — wenzelm / hgweb
more parallel; — wenzelm / hgweb
more parallel; — wenzelm / hgweb
contributors — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
hide the internal abbreviations MR and MB — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
optimize RBT_Impl — mraszyk / hgweb
merged — wenzelm / hgweb
more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup); — wenzelm / hgweb
tuned signature: more types; — wenzelm / hgweb
clarified signature: proper order; — wenzelm / hgweb
clarified signature: more explicit types; — wenzelm / hgweb
tuned; — wenzelm / hgweb
clarified signature: no symbol markup within XML attributes; — wenzelm / hgweb
clarified signature; — wenzelm / hgweb
tuned signature; — wenzelm / hgweb
bundle more libraries from scala-2.12.x, notably for Isabelle/MMT; — wenzelm / hgweb
provide naproche-20210129; — wenzelm / hgweb
more robust type signatures, notably for the sake of haskell-stack-trace-plugin-0.1.1.1; — wenzelm / hgweb
tuned signature (e.g. see HTML.control_block in Isabelle/Scala); — wenzelm / hgweb
proper Isabelle environment (amending 31fbde3baa97); — wenzelm / hgweb
updated to jdk-15.0.2+7; — wenzelm / hgweb
follow Phabricator update 2021 Week 4; — wenzelm / hgweb
more NEWS; — wenzelm / hgweb
more uniform directory layout for macOS;
uniform Isabelle_app executable + lib/scripts/Isabelle_app for Linux and macOS;
proper support for Apple "Files and Folders" security via x86_64-darwin executable (which is still able to launch arm64-darwin Java); — wenzelm / hgweb
more generic Isabelle_app; — wenzelm / hgweb
prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc); — wenzelm / hgweb
more robust; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned; — wenzelm / hgweb
provide jdk-11.0.10+9.tar.gz LTS for testing (inactive); — wenzelm / hgweb

#34 (Feb 7, 2021, 12:14:00 AM)

merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
merge from afp-2020 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
fixed category for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
Backed out changeset 4450302adc70 — Manuel Eberl <eberlm@in.tum.de> / hgweb
fixed category for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
sitegen for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
New entry: Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
paragraph tags in the abstract of IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
tidying of IsaGeoCoq including a shorter abstract and revised title — paulson <lp15@cam.ac.uk> / hgweb
website for IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
new entry IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
hide MB abbreviation — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
integrate RBT_Impl optimizations — mraszyk / hgweb

#33 (Jan 31, 2021, 12:14:00 AM)

Simpler proof — nipkow / hgweb
more robust: support other_isabelle.init_settings for build_history before b93404a4c3dd; — wenzelm / hgweb
more robust: defer error in sessions structure to build process; — wenzelm / hgweb
merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS; — wenzelm / hgweb
Added tag Isabelle2021-RC3 for changeset 02422c9add5e — wenzelm / hgweb
provide naproche-20210124 (inactive); — wenzelm / hgweb
follow stackage update; — wenzelm / hgweb
tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit; — wenzelm / hgweb
more operations for client connection; — wenzelm / hgweb
fewer warnings, notably in Naproche-SAD; — wenzelm / hgweb
suppress bundled Naproche-SAD component: it is in conflict with building the same from sources; — wenzelm / hgweb
more robust etc/settings; — wenzelm / hgweb
IDE support for Naproche-SAD; — wenzelm / hgweb
proper path; — wenzelm / hgweb
support isabelle components -u and -x; — wenzelm / hgweb
proper typescript version, required for "vsce package"; — wenzelm / hgweb
auto-update; — wenzelm / hgweb
auto-update; — wenzelm / hgweb
proper type constraint; — wenzelm / hgweb
VSCode extension for official Isabelle release; — wenzelm / hgweb
proper message; — wenzelm / hgweb
unused; — wenzelm / hgweb
proper heap_free; — wenzelm / hgweb
suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff); — wenzelm / hgweb
clarified documentation concerning macOS Big Sur; — wenzelm / hgweb
more systematic java-gui-setup, also for "isabelle jedit" command-line tool; — wenzelm / hgweb
updated to flatlaf-1.0-rc1; — wenzelm / hgweb
tuned; — wenzelm / hgweb
tuned proofs; — wenzelm / hgweb
tuned; — wenzelm / hgweb
obsolete; — wenzelm / hgweb
clarified platforms; — wenzelm / hgweb
more NEWS; — wenzelm / hgweb
workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g. Find on top of main View); — wenzelm / hgweb
clarified app identification, potentially relevant for macOS "defaults"; — wenzelm / hgweb
updated documentation: HIDPI works smoothly thanks to FlatLaf; — wenzelm / hgweb
updated for release; — wenzelm / hgweb
updated screenshot; — wenzelm / hgweb
clarified reports before errors: support completion of bibtex entries in Isabelle/Scala (amending d01ea9e3bd2d); — wenzelm / hgweb
tuned; — wenzelm / hgweb
proper theory_long_name; — wenzelm / hgweb
updated screenshots; — wenzelm / hgweb
more robust GUI, notably for Big Sur full-screen where the hypersearch panel becomes a separate maximized window; — wenzelm / hgweb
revert 1105c42722dc on isabelle-release branch; — wenzelm / hgweb

#33 (Jan 31, 2021, 12:14:00 AM)

Merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
Small update to Optics document. — Simon Foster <simon.foster@york.ac.uk> / hgweb
merged — wenzelm / hgweb
more generous timeout (25min CPU time); — wenzelm / hgweb
non-executable files; — wenzelm / hgweb
Added metadata for previous commit (Optics). — Simon Foster <simon.foster@york.ac.uk> / hgweb
Addition of theorems throughout, particularly for prisms.
New "chantype" command allows the definition of an algebraic datatype with generated prisms.
New "dataspace" command allows the definition of a local-based state space, including lenses and prisms.
Addition of various examples. — Simon Foster <simon.foster@york.ac.uk> / hgweb
adjustments for Word_Lib updates — kleing / hgweb
sync with l4v — kleing / hgweb
allow instance for nat

(by Florian) — kleing / hgweb
merge from afp-2020 — kleing / hgweb
New entry JinjaDCI — nipkow / hgweb

#31 (Jan 17, 2021, 12:14:00 AM)

back to post-release mode; — wenzelm / hgweb
Added tag Isabelle2021-RC2 for changeset 802647edfe7b — wenzelm / hgweb
tuned; — wenzelm / hgweb
avoid Unicode quotes; — wenzelm / hgweb
clarified pretty margin: attempt to avoid scrollbar; — wenzelm / hgweb
more documentation; — wenzelm / hgweb
more informative errors: simplify diagnosis of spurious failures reported by users; — wenzelm / hgweb