Page MenuHomeIsabelle/Phabricator
Feed All Stories

Dec 16 2019

nipkow committed rAFPca5f1ca3a8e5: tuned.
tuned
Dec 16 2019, 12:59 PM
nipkow committed rAFPdc000cacc8fa: tuned.
tuned
Dec 16 2019, 11:01 AM
nipkow committed rAFP9282ad6144da: new theory in Priority_Queue_Braun.
new theory in Priority_Queue_Braun
Dec 16 2019, 11:00 AM
nipkow committed rAFPfd8327b801a2: merged.
merged
Dec 16 2019, 11:00 AM
nipkow committed rAFP0e1e232a338a: tuned.
tuned
Dec 16 2019, 11:00 AM

Dec 14 2019

makarius committed rISABELLE5b3a813853bb: tuned message;.
tuned message;
Dec 14 2019, 11:33 PM
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 14 2019, 11:33 PM

Dec 13 2019

blanchette committed rAFPaecde7853101: tuning.
tuning
Dec 13 2019, 11:02 AM
Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFP04690e89d173: EPO: switch size measure.
EPO: switch size measure
Dec 13 2019, 11:02 AM

Dec 12 2019

makarius committed rISABELLE2e873da296ae: more documentation;.
more documentation;
Dec 12 2019, 4:19 PM
makarius committed rISABELLE197aa6b57a83: more documentation;.
more documentation;
Dec 12 2019, 4:19 PM
makarius committed rISABELLE74cabc06cf2d: proper support for multiple installations;.
proper support for multiple installations;
Dec 12 2019, 4:19 PM
makarius committed rISABELLEb4401dfd6544: clarified "isabelle phabricator -l": avoid surprise with non-existent default….
clarified "isabelle phabricator -l": avoid surprise with non-existent default…
Dec 12 2019, 4:19 PM

Dec 11 2019

makarius committed rISABELLE18f4061fd817: tuned index.html;.
tuned index.html;
Dec 11 2019, 11:06 PM
makarius committed rISABELLE5212ca49598a: more robust;.
more robust;
Dec 11 2019, 10:16 PM
makarius committed rISABELLE6b8cbdc9713b: more robust;.
more robust;
Dec 11 2019, 10:16 PM
makarius added members for isabelle-repository: florian.haftmann, lukas.bulwahn.
Dec 11 2019, 9:32 PM
wenzelm committed rISABELLE1e7319957408: clarified website: redirect to isabelle-dev Phabricator Overview;.
clarified website: redirect to isabelle-dev Phabricator Overview;
Dec 11 2019, 7:17 PM
wenzelm committed rISABELLE58aa62b8c6d3: more documentation;.
more documentation;
Dec 11 2019, 4:49 PM
wenzelm committed rISABELLE3184dbad4d7d: tuned;.
tuned;
Dec 11 2019, 4:49 PM
wenzelm committed rISABELLE7df5c110a43c: support database dump;.
support database dump;
Dec 11 2019, 4:48 PM

Dec 10 2019

wenzelm committed rISABELLEe2fb60756fb8: proper check of Linux version;.
proper check of Linux version;
Dec 10 2019, 9:36 PM
wenzelm committed rISABELLEd5751eb5cc57: tuned;.
tuned;
Dec 10 2019, 9:36 PM
wenzelm committed rISABELLE8451c86ffa85: proper mysql user setup: avoid superuser powers in production;.
proper mysql user setup: avoid superuser powers in production;
Dec 10 2019, 9:36 PM
wenzelm committed rISABELLE6ca561001244: support for pwgen;.
support for pwgen;
Dec 10 2019, 9:36 PM
traytel committed rISABELLE0c454a5d125d: NEWS, CONTRIBUTORS, and documentation.
NEWS, CONTRIBUTORS, and documentation
Dec 10 2019, 9:16 AM
traytel committed rISABELLE35a92ce0b94e: an extensive example for lift_bnf across quotients.
an extensive example for lift_bnf across quotients
Dec 10 2019, 9:16 AM
traytel committed rISABELLEa30278c8585f: extension of lift_bnf to support quotient types.
extension of lift_bnf to support quotient types
Dec 10 2019, 9:16 AM
traytel committed rISABELLE4765fec43414: unfold intermediate (internal) pred definitions.
unfold intermediate (internal) pred definitions
Dec 10 2019, 9:16 AM
traytel committed rAFPf9cbe0d87965: adapt to isabelle/a30278c8585f; tuned whitespace.
adapt to isabelle/a30278c8585f; tuned whitespace
Dec 10 2019, 9:16 AM

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
Dec 9 2019, 8:18 PM
paulson <lp15@cam.ac.uk> committed rISABELLE308baf6b450a: corrected some confusing terminology / notation.
corrected some confusing terminology / notation
Dec 9 2019, 5:37 PM
paulson <lp15@cam.ac.uk> committed rISABELLE09aee7f5b447: Ramsey with multiple colours and arbitrary exponents.
Ramsey with multiple colours and arbitrary exponents
Dec 9 2019, 5:13 PM
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)
Dec 9 2019, 4:37 PM
wenzelm committed rISABELLEb1f3e86a4745: clarified signature: store full theory name;.
clarified signature: store full theory name;
Dec 9 2019, 11:22 AM

Dec 8 2019

nipkow committed rISABELLEdd74e0558fd1: merged.
merged
Dec 8 2019, 5:45 PM
nipkow committed rISABELLE4258ee13f5d4: moved lemmas.
moved lemmas
Dec 8 2019, 5:45 PM

Dec 6 2019

wenzelm committed rISABELLEa9ad4a954cb7: merged.
merged
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLEa62431901140: suppress record types: not working properly;.
suppress record types: not working properly;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLEc5914bdd896b: removed junk;.
removed junk;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLE297d24fb262c: discontinued somewhat pointless options;.
discontinued somewhat pointless options;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLE877316c54ed3: clarified signature;.
clarified signature;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLEbd93c71521a0: tuned signature;.
tuned signature;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLEadf5e53d2b2b: export datatypes;.
export datatypes;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLE6e0ff949073e: clarified modules;.
clarified modules;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLE30db0523f9b0: misc tuning and clarification: proper check of datatype kind;.
misc tuning and clarification: proper check of datatype kind;
Dec 6 2019, 8:29 PM
wenzelm committed rISABELLEe5664a75f4b5: clarified modules;.
clarified modules;
Dec 6 2019, 8:29 PM
nipkow committed rAFP429a712d7c4d: adapted to devel.
adapted to devel
Dec 6 2019, 7:00 PM
nipkow committed rISABELLE38457af660bc: cleaning.
cleaning
Dec 6 2019, 6:24 PM
nipkow committed rISABELLE5b7c85586eb1: tuned.
tuned
Dec 6 2019, 2:37 PM

Dec 5 2019

nipkow committed rISABELLEec5090faf541: separated Affine theory from Convex.
separated Affine theory from Convex
Dec 5 2019, 10:31 PM
nipkow committed rISABELLEd9e747cafb04: merged.
merged
Dec 5 2019, 7:54 PM
nipkow committed rISABELLE67880e7ee08d: tuned.
tuned
Dec 5 2019, 7:54 PM
haftmann committed rISABELLEacc6cb1a1a67: proper table data structure.
proper table data structure
Dec 5 2019, 3:54 PM
haftmann committed rISABELLE9612115e06d1: removed some vain declarations.
removed some vain declarations
Dec 5 2019, 3:54 PM
nipkow committed rISABELLEda73ee760643: merged.
merged
Dec 5 2019, 1:51 PM
nipkow committed rISABELLE6c1ed478605e: made Starlike independent of Abstract_Limits.
made Starlike independent of Abstract_Limits
Dec 5 2019, 1:51 PM
haftmann committed rISABELLEd12c58e12c51: more direct accessors for simpset.
more direct accessors for simpset
Dec 5 2019, 1:10 PM
davetbutler committed rAFP7c33f283cfef: MPC update ETP and perfect sec rename.
MPC update ETP and perfect sec rename
Dec 5 2019, 12:33 PM
haftmann committed rISABELLEf1838cf9f139: regular merge with no historization, in accordance with regular update.
regular merge with no historization, in accordance with regular update
Dec 5 2019, 7:50 AM
nipkow committed rISABELLEda28fd2852ed: moved starlike where it belongs.
moved starlike where it belongs
Dec 5 2019, 6:59 AM

Dec 4 2019

wenzelm committed rISABELLE7b9ff966974f: merged.
merged
Dec 4 2019, 8:08 PM
wenzelm committed rISABELLEdafa5fce70f1: clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many….
clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many…
Dec 4 2019, 8:08 PM
nipkow committed rISABELLE095cf95d7725: moved segment lemmas where they belong.
moved segment lemmas where they belong
Dec 4 2019, 7:24 PM
Peter Lammich committed rAFP8c3387faaeed: Fixed CAVA-Impl to accomodate for generalized Gabow_GBG.
Fixed CAVA-Impl to accomodate for generalized Gabow_GBG
Dec 4 2019, 6:34 PM
Peter Lammich committed rAFP3049a0ad195d: merged.
merged
Dec 4 2019, 6:34 PM
Peter Lammich committed rAFP7d5c0f2b46b5: Generalized Gabow-SCC to arbitrary refinements for nodes.
Generalized Gabow-SCC to arbitrary refinements for nodes
Dec 4 2019, 6:34 PM
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.
Dec 4 2019, 5:36 PM
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
Dec 4 2019, 5:36 PM
nipkow committed rISABELLEbe2c2bfa54a0: merged.
merged
Dec 4 2019, 3:37 PM
nipkow committed rISABELLEdc767054de47: moved lemmas.
moved lemmas
Dec 4 2019, 3:37 PM
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
Dec 4 2019, 1:53 PM
paulson committed rISABELLEe9a4bd0a836e: merged.
merged
Dec 4 2019, 1:51 PM
paulson <lp15@cam.ac.uk> committed rISABELLE9adb1e16b2a6: two new theorems.
two new theorems
Dec 4 2019, 1:51 PM
nipkow committed rISABELLE1249859d23dd: moved lemma.
moved lemma
Dec 4 2019, 1:08 PM
traytel committed rISABELLE54a7ad860a76: made internal name generation in case expressions more robust.
made internal name generation in case expressions more robust
Dec 4 2019, 9:05 AM

Dec 3 2019

wenzelm committed rISABELLEd411d5c84a4b: merged.
merged
Dec 3 2019, 7:37 PM
wenzelm committed rISABELLE2bc39c80a95d: clarified export of consts: recursion is accessible via spec_rules;.
clarified export of consts: recursion is accessible via spec_rules;
Dec 3 2019, 7:37 PM
wenzelm committed rISABELLE4dfb7c937126: more operations;.
more operations;
Dec 3 2019, 7:37 PM
pruvisto committed rISABELLE6f8422385878: Removed orphaned theory from HOL-Analysis.
Removed orphaned theory from HOL-Analysis
Dec 3 2019, 5:15 PM
wenzelm committed rAFP801b10285bb6: merged.
merged
Dec 3 2019, 3:36 PM
wenzelm committed rAFPde5e63a46b97: adapted to Isabelle/5727bcc3c47c;.
adapted to Isabelle/5727bcc3c47c;
Dec 3 2019, 3:36 PM
wenzelm committed rISABELLE35e465677a26: merged.
merged
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE73b313432d8a: clarified position for spec rule: like entity;.
clarified position for spec rule: like entity;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE2dee5cd42fde: clarified name: avoid clashes;.
clarified name: avoid clashes;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE37eb175895c5: proper treatment of variable names;.
proper treatment of variable names;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLEe64c249d3d98: proper dynamic position of application context, e.g. relevant for….
proper dynamic position of application context, e.g. relevant for…
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE39ccdbbed539: more informative spec rules;.
more informative spec rules;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE5727bcc3c47c: proper spec_rule name via naming/binding/Morphism.binding;.
proper spec_rule name via naming/binding/Morphism.binding;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE475510f1a280: more robust;.
more robust;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE7d522732b7f2: more informative export;.
more informative export;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE8508cc7f79aa: tuned comment;.
tuned comment;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE66fa99c85095: tuned signature -- following Export_Theory.Spec_Rule in Scala;.
tuned signature -- following Export_Theory.Spec_Rule in Scala;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE5e0050eb64f2: clarified export of spec rules: more like locale;.
clarified export of spec rules: more like locale;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE8af82f3e03c9: formal position for spec rule (not significant for equality);.
formal position for spec rule (not significant for equality);
Dec 3 2019, 3:35 PM
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…
Dec 3 2019, 3:35 PM
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…
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLEabb0d984abbc: tuned -- avoid confusion of fun_t with fun_lhs;.
tuned -- avoid confusion of fun_t with fun_lhs;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLEeb5591ca90da: avoid shadowing of local bindings -- more maintainable;.
avoid shadowing of local bindings -- more maintainable;
Dec 3 2019, 3:35 PM
wenzelm committed rISABELLE785610ad6bfa: export spec rules;.
export spec rules;
Dec 3 2019, 3:35 PM