- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Dec 16 2019
Dec 16 2019
nipkow committed rAFP9282ad6144da: new theory in Priority_Queue_Braun.
new theory in Priority_Queue_Braun
Dec 14 2019
Dec 14 2019
makarius committed rISABELLE5a2033fc8f3d: avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on….
avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on…
Dec 13 2019
Dec 13 2019
Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFP04690e89d173: EPO: switch size measure.
EPO: switch size measure
Dec 12 2019
Dec 12 2019
more documentation;
more documentation;
proper support for multiple installations;
makarius committed rISABELLEb4401dfd6544: clarified "isabelle phabricator -l": avoid surprise with non-existent default….
clarified "isabelle phabricator -l": avoid surprise with non-existent default…
Dec 11 2019
Dec 11 2019
wenzelm committed rISABELLE1e7319957408: clarified website: redirect to isabelle-dev Phabricator Overview;.
clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm committed rISABELLE58aa62b8c6d3: more documentation;.
more documentation;
wenzelm committed rISABELLE7df5c110a43c: support database dump;.
support database dump;
Dec 10 2019
Dec 10 2019
wenzelm committed rISABELLEe2fb60756fb8: proper check of Linux version;.
proper check of Linux version;
wenzelm committed rISABELLE8451c86ffa85: proper mysql user setup: avoid superuser powers in production;.
proper mysql user setup: avoid superuser powers in production;
NEWS, CONTRIBUTORS, and documentation
an extensive example for lift_bnf across quotients
extension of lift_bnf to support quotient types
unfold intermediate (internal) pred definitions
adapt to isabelle/a30278c8585f; tuned whitespace
Dec 9 2019
Dec 9 2019
paulson <lp15@cam.ac.uk> committed rAFP712c4cf1b3c1: fixed a theory sensitive to ext_funcset_to_sing_iff.
fixed a theory sensitive to ext_funcset_to_sing_iff
paulson <lp15@cam.ac.uk> committed rISABELLE308baf6b450a: corrected some confusing terminology / notation.
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk> committed rISABELLE09aee7f5b447: Ramsey with multiple colours and arbitrary exponents.
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk> committed rISABELLEd67924987c34: a few new and tidier proofs (mostly about finite sets).
a few new and tidier proofs (mostly about finite sets)
wenzelm committed rISABELLEb1f3e86a4745: clarified signature: store full theory name;.
clarified signature: store full theory name;
Dec 8 2019
Dec 8 2019
Dec 6 2019
Dec 6 2019
wenzelm committed rISABELLEa62431901140: suppress record types: not working properly;.
suppress record types: not working properly;
wenzelm committed rISABELLE297d24fb262c: discontinued somewhat pointless options;.
discontinued somewhat pointless options;
wenzelm committed rISABELLE877316c54ed3: clarified signature;.
clarified signature;
wenzelm committed rISABELLE30db0523f9b0: misc tuning and clarification: proper check of datatype kind;.
misc tuning and clarification: proper check of datatype kind;
Dec 5 2019
Dec 5 2019
nipkow committed rISABELLEec5090faf541: separated Affine theory from Convex.
separated Affine theory from Convex
haftmann committed rISABELLEacc6cb1a1a67: proper table data structure.
proper table data structure
haftmann committed rISABELLE9612115e06d1: removed some vain declarations.
removed some vain declarations
nipkow committed rISABELLE6c1ed478605e: made Starlike independent of Abstract_Limits.
made Starlike independent of Abstract_Limits
haftmann committed rISABELLEd12c58e12c51: more direct accessors for simpset.
more direct accessors for simpset
davetbutler committed rAFP7c33f283cfef: MPC update ETP and perfect sec rename.
MPC update ETP and perfect sec rename
haftmann committed rISABELLEf1838cf9f139: regular merge with no historization, in accordance with regular update.
regular merge with no historization, in accordance with regular update
nipkow committed rISABELLEda28fd2852ed: moved starlike where it belongs.
moved starlike where it belongs
Dec 4 2019
Dec 4 2019
wenzelm committed rISABELLEdafa5fce70f1: clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many….
clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many…
nipkow committed rISABELLE095cf95d7725: moved segment lemmas where they belong.
moved segment lemmas where they belong
Peter Lammich committed rAFP8c3387faaeed: Fixed CAVA-Impl to accomodate for generalized Gabow_GBG.
Fixed CAVA-Impl to accomodate for generalized Gabow_GBG
Peter Lammich committed rAFP7d5c0f2b46b5: Generalized Gabow-SCC to arbitrary refinements for nodes.
Generalized Gabow-SCC to arbitrary refinements for nodes
David Matthews <dm@prolingua.co.uk> committed rPOLYML850ca1289823: Rebuild Makefile.in after merge. (authored by David Matthews <dm@prolingua.co.uk>).
Rebuild Makefile.in after merge.
David Matthews <dm@prolingua.co.uk> committed rPOLYMLbd0917074271: Merge branch 'master' into GCPercent (authored by David Matthews <dm@prolingua.co.uk>).
Merge branch 'master' into GCPercent
paulson <lp15@cam.ac.uk> committed rAFP3768c25e32fa: Removal of material that has been transferred to the main libraries.
Removal of material that has been transferred to the main libraries
paulson <lp15@cam.ac.uk> committed rISABELLE9adb1e16b2a6: two new theorems.
two new theorems
traytel committed rISABELLE54a7ad860a76: made internal name generation in case expressions more robust.
made internal name generation in case expressions more robust
Dec 3 2019
Dec 3 2019
wenzelm committed rISABELLE2bc39c80a95d: clarified export of consts: recursion is accessible via spec_rules;.
clarified export of consts: recursion is accessible via spec_rules;
Removed orphaned theory from HOL-Analysis
wenzelm committed rAFPde5e63a46b97: adapted to Isabelle/5727bcc3c47c;.
adapted to Isabelle/5727bcc3c47c;
wenzelm committed rISABELLE73b313432d8a: clarified position for spec rule: like entity;.
clarified position for spec rule: like entity;
wenzelm committed rISABELLE2dee5cd42fde: clarified name: avoid clashes;.
clarified name: avoid clashes;
wenzelm committed rISABELLE37eb175895c5: proper treatment of variable names;.
proper treatment of variable names;
wenzelm committed rISABELLEe64c249d3d98: proper dynamic position of application context, e.g. relevant for….
proper dynamic position of application context, e.g. relevant for…
wenzelm committed rISABELLE39ccdbbed539: more informative spec rules;.
more informative spec rules;
wenzelm committed rISABELLE5727bcc3c47c: proper spec_rule name via naming/binding/Morphism.binding;.
proper spec_rule name via naming/binding/Morphism.binding;
wenzelm committed rISABELLE7d522732b7f2: more informative export;.
more informative export;
wenzelm committed rISABELLE66fa99c85095: tuned signature -- following Export_Theory.Spec_Rule in Scala;.
tuned signature -- following Export_Theory.Spec_Rule in Scala;
wenzelm committed rISABELLE5e0050eb64f2: clarified export of spec rules: more like locale;.
clarified export of spec rules: more like locale;
wenzelm committed rISABELLE8af82f3e03c9: formal position for spec rule (not significant for equality);.
formal position for spec rule (not significant for equality);
wenzelm committed rISABELLE20dce31fe7f4: proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o….
proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o…
wenzelm committed rISABELLE95e12ecdcb5f: proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o….
proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o…
wenzelm committed rISABELLEabb0d984abbc: tuned -- avoid confusion of fun_t with fun_lhs;.
tuned -- avoid confusion of fun_t with fun_lhs;
avoid shadowing of local bindings -- more maintainable;