Page MenuHomeIsabelle/Phabricator
Feed All Stories

Feb 28 2020

makarius committed rISABELLE4c3eedc8e0f7: NEWS;.
NEWS;
Feb 28 2020, 10:23 PM
makarius committed rISABELLEa296d3697e50: updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);.
updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
Feb 28 2020, 10:23 PM
makarius committed rWEBSITE3fe544274896: updated for release;.
updated for release;
Feb 28 2020, 4:41 PM
makarius committed rISABELLE0a20dd339a05: tuned;.
tuned;
Feb 28 2020, 4:40 PM
Asta Halkjær From <s144442@student.dtu.dk> committed rAFPb8e1eebb4b17: merge.
merge
Feb 28 2020, 1:19 PM
Asta Halkjær From <s144442@student.dtu.dk> committed rAFPf5a944f4cf54: Add inputenc.
Add inputenc
Feb 28 2020, 1:19 PM

Feb 27 2020

dcjm committed rPOLYML6025c250b4f1: Change Posix.Process.exit to use the same underlying call as OS.Process. (authored by dcjm).
Change Posix.Process.exit to use the same underlying call as OS.Process.
Feb 27 2020, 9:10 PM
dcjm committed rPOLYML744d14ffd49b: Fix bug found by Makarius in generated code. It seems to have been introduced… (authored by dcjm).
Fix bug found by Makarius in generated code. It seems to have been introduced…
Feb 27 2020, 9:10 PM
makarius committed rISABELLE3488c0eb4cc8: more complete signature;.
more complete signature;
Feb 27 2020, 1:32 PM
makarius committed rISABELLEe8da4a8d364a: more complete signature;.
more complete signature;
Feb 27 2020, 1:32 PM
makarius committed rISABELLEcf39375d5cfe: clarified versions -- more reproducible build;.
clarified versions -- more reproducible build;
Feb 27 2020, 12:28 PM
nipkow committed rISABELLE059c55b61734: removed dead lemma.
removed dead lemma
Feb 27 2020, 12:19 PM

Feb 26 2020

nipkow committed rISABELLE0e1b9b308d8f: simplified proofs.
simplified proofs
Feb 26 2020, 11:50 PM
makarius committed rISABELLE29e297fd5473: updated for release;.
updated for release;
Feb 26 2020, 7:51 PM
makarius committed rISABELLEbb82dd4d19f6: updated for release;.
updated for release;
Feb 26 2020, 7:51 PM
makarius closed T3: Adapt Isabelle/VSCode to Webview API as Resolved.

See Isabelle/be84312a2d53 to Isabelle/aa7b0a5e9fe3

Feb 26 2020, 4:30 PM · isabelle-release
makarius committed rISABELLE6de04d21c26b: merged.
merged
Feb 26 2020, 4:29 PM
makarius committed rISABELLEaa7b0a5e9fe3: updated for release;.
updated for release;
Feb 26 2020, 4:29 PM
makarius committed rISABELLEbb1c829534ba: obsolete;.
obsolete;
Feb 26 2020, 4:29 PM
makarius committed rISABELLEea6adb18730d: updated version;.
updated version;
Feb 26 2020, 4:29 PM
makarius committed rISABELLE6aa2dc263912: less ambitious preview: discontinued preview-update / preview-source which did….
less ambitious preview: discontinued preview-update / preview-source which did…
Feb 26 2020, 4:29 PM
makarius committed rISABELLE5c0293826dc8: misc tuning and clarification;.
misc tuning and clarification;
Feb 26 2020, 4:29 PM
makarius committed rISABELLEecefde4f9103: proper message passing -- discontinued obsolete auxiliary commands;.
proper message passing -- discontinued obsolete auxiliary commands;
Feb 26 2020, 4:29 PM
makarius committed rISABELLE24e3adaee6ec: obsolete;.
obsolete;
Feb 26 2020, 4:29 PM
makarius committed rISABELLE7a867a38712a: clarified Panel;.
clarified Panel;
Feb 26 2020, 4:28 PM
makarius committed rISABELLEfe1b19bf5fef: removed duplicate (amending 5763d9a2f47d, 5aa9cb83e70e);.
removed duplicate (amending 5763d9a2f47d, 5aa9cb83e70e);
Feb 26 2020, 4:28 PM
makarius committed rISABELLEbe84312a2d53: update to WebviewPanel API, following initial version by Peter Zeller;.
update to WebviewPanel API, following initial version by Peter Zeller;
Feb 26 2020, 4:28 PM
paulson <lp15@cam.ac.uk> committed rISABELLEc213d067e60f: Moved a number of general-purpose lemmas into HOL.
Moved a number of general-purpose lemmas into HOL
Feb 26 2020, 1:22 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP27ea89db8cd6: continued working on automata tool and benchmarks.
continued working on automata tool and benchmarks
Feb 26 2020, 6:45 AM

Feb 25 2020

makarius committed rISABELLEc06604896c3d: more robust shutdown while Isabelle_Process is starting up, e.g. quit after….
more robust shutdown while Isabelle_Process is starting up, e.g. quit after…
Feb 25 2020, 6:09 PM
makarius triaged T17: Proper treatment of hidden polymorphism in proof terms as Normal priority.
Feb 25 2020, 12:00 PM · isabelle-release
makarius triaged T16: Clarify indentation after 'oops' as Normal priority.
Feb 25 2020, 11:52 AM
makarius updated the task description for T13: Isabelle/jEdit indenting.
Feb 25 2020, 11:25 AM

Feb 24 2020

traytel committed rISABELLEb94053ca8d77: merged.
merged
Feb 24 2020, 11:18 PM
traytel committed rISABELLEd7ef73df3d15: lift BNF witnesses for quotients (unless better ones are specified by the user).
lift BNF witnesses for quotients (unless better ones are specified by the user)
Feb 24 2020, 11:18 PM
makarius committed rISABELLE53fcbede7bf7: more robust (amending add9a9f6a290): proper syntax error instead of exception….
more robust (amending add9a9f6a290): proper syntax error instead of exception…
Feb 24 2020, 10:34 PM
nipkow committed rISABELLE708d301205fe: merged.
merged
Feb 24 2020, 9:44 PM
nipkow committed rISABELLEac70b63785bb: tuned var names (avoid h).
tuned var names (avoid h)
Feb 24 2020, 9:44 PM
makarius committed rISABELLE910a081cca74: more position information for oracles (e.g. "skip_proof" for 'sorry'), requires….
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires…
Feb 24 2020, 9:12 PM
paulson <lp15@cam.ac.uk> committed rAFP89ba7ebaf43f: New and/or strengthened lemmas.
New and/or strengthened lemmas
Feb 24 2020, 1:38 PM
paulson <lp15@cam.ac.uk> committed rISABELLE4a04b6bd628b: a few new lemmas.
a few new lemmas
Feb 24 2020, 1:17 PM

Feb 23 2020

"Eugene W. Stark <stark@cs.stonybrook.edu>" committed rAFP76aa4d49a895: Demote some simps that were not pulling their weight..
Demote some simps that were not pulling their weight.
Feb 23 2020, 5:39 PM
"Eugene W. Stark <stark@cs.stonybrook.edu>" committed rAFP4b4d09cb8a4c: Tweaks, mostly in search of speedup..
Tweaks, mostly in search of speedup.
Feb 23 2020, 1:17 AM

Feb 21 2020

nipkow committed rISABELLEa31a9da43694: tuned deletion.
tuned deletion
Feb 21 2020, 5:53 PM

Feb 20 2020

traytel committed rISABELLEed8d50969995: merged.
merged
Feb 20 2020, 9:14 AM
traytel committed rISABELLE5e25a693c5cf: additional lemmas about alw and suntil (by Michael Foster).
additional lemmas about alw and suntil (by Michael Foster)
Feb 20 2020, 9:14 AM

Feb 19 2020

makarius triaged T15: Localized record package as Normal priority.
Feb 19 2020, 8:48 PM
makarius triaged T14: Fully localized type abbreviations as Wishlist priority.
Feb 19 2020, 8:43 PM
makarius committed rISABELLE8f628d216ea1: proper print mode for function_space notation (amending d68b705719ce);.
proper print mode for function_space notation (amending d68b705719ce);
Feb 19 2020, 8:07 PM
makarius committed rISABELLE4876e6f62fe5: proper file name (amending ce3409dfb18c);.
proper file name (amending ce3409dfb18c);
Feb 19 2020, 4:05 PM

Feb 18 2020

makarius renamed T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow from Evaluate https://discourse.org as replacement for mailman, stackoverflow, zulip to Evaluate https://discourse.org as replacement for mailman, stackoverflow.
Feb 18 2020, 9:08 PM
nipkow committed rISABELLEdd7e398a04ae: merged.
merged
Feb 18 2020, 6:08 PM
nipkow committed rISABELLEd6e139438e4a: tuned proof.
tuned proof
Feb 18 2020, 6:08 PM
makarius committed rISABELLE09c850e82258: more robust pretty printing of broken YXML, e.g. single "\^E";.
more robust pretty printing of broken YXML, e.g. single "\^E";
Feb 18 2020, 4:08 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP2d4667e525c2: merged.
merged
Feb 18 2020, 2:18 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFPcd0b90f7688d: added equivalence and automata tool.
added equivalence and automata tool
Feb 18 2020, 2:18 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP6119bf12038f: streamlined NBA translation.
streamlined NBA translation
Feb 18 2020, 2:18 PM
pruvisto committed rAFPbf1920e1bc60: make Poincare_Disc build on Complex_Geometry.
make Poincare_Disc build on Complex_Geometry
Feb 18 2020, 12:10 PM
pruvisto committed rAFPc35f8cc3dda7: repaired broken proofs in Skip_Lists; removed unfinished experimental thy file.
repaired broken proofs in Skip_Lists; removed unfinished experimental thy file
Feb 18 2020, 12:01 PM
lukasstevens added a comment to T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.

Zulipchat (https://zulipchat.com/) is a chat service that has an interactive eMail-like threading model. Content is formatted in markdown complete with code formatting and more. With its filter mechanisms, one can easily concentrate on single threads or mute threads that one is no longer interested in. Since Zulipchat is open-source, it is possible to self-host it and use a variety of authentication schemes (https://zulip.readthedocs.io/en/stable/production/authentication-methods.html).

Feb 18 2020, 11:10 AM

Feb 17 2020

makarius committed rISABELLE35b2d407e558: merged.
merged
Feb 17 2020, 9:11 PM
makarius committed rISABELLEb2c9f94e025f: proper sort constraints for strip_shyps, for sort relations used in….
proper sort constraints for strip_shyps, for sort relations used in…
Feb 17 2020, 9:11 PM
makarius edited Description on isabelle-release.
Feb 17 2020, 2:27 PM
makarius edited Description on isabelle-release.
Feb 17 2020, 2:27 PM
makarius edited Description on isabelle-release.
Feb 17 2020, 2:26 PM
paulson <lp15@cam.ac.uk> committed rAFP29f2271f9455: a few new lemmas.
a few new lemmas
Feb 17 2020, 1:22 PM
paulson committed rISABELLE7b8a6840e85f: merged.
merged
Feb 17 2020, 12:33 PM
paulson <lp15@cam.ac.uk> committed rISABELLE9edb7fb69bc2: a few new lemmas.
a few new lemmas
Feb 17 2020, 12:33 PM
makarius committed rISABELLEfb08117a106b: tuned;.
tuned;
Feb 17 2020, 12:06 PM
kleing triaged T13: Isabelle/jEdit indenting as Normal priority.
Feb 17 2020, 4:10 AM
Julian Brunner <julianbrunner@gmail.com> committed rAFPc9a73112a393: updated root file.
updated root file
Feb 17 2020, 12:37 AM
Julian Brunner <julianbrunner@gmail.com> committed rAFP06bb4c12bc7b: refactoring.
refactoring
Feb 17 2020, 12:37 AM

Feb 16 2020

nipkow committed rISABELLEefcd6742ea9c: merged.
merged
Feb 16 2020, 9:11 PM
nipkow committed rISABELLE3cf130a896a3: lemmas about "card A = 2"; prefer iff to implications.
lemmas about "card A = 2"; prefer iff to implications
Feb 16 2020, 9:11 PM
makarius committed rISABELLE404624eb3a22: NEWS;.
NEWS;
Feb 16 2020, 8:18 PM
makarius committed rISABELLE439410bf4519: proper sort constraints for strip_shyps, which implicitly performs type….
proper sort constraints for strip_shyps, which implicitly performs type…
Feb 16 2020, 8:18 PM

Feb 15 2020

makarius committed rISABELLE91340a6bf401: NEWS;.
NEWS;
Feb 15 2020, 9:22 PM
makarius added a member for isabelle-repository: kleing.
Feb 15 2020, 5:13 PM
"Eugene W. Stark <stark@cs.stonybrook.edu>" committed rAFPecd9de819957: Update change history..
Update change history.
Feb 15 2020, 8:27 AM
"Eugene W. Stark <stark@cs.stonybrook.edu>" committed rAFPa51840d36867: Move ConcreteCategory.thy from Bicategory to Category3 and use it….
Move ConcreteCategory.thy from Bicategory to Category3 and use it…
Feb 15 2020, 8:27 AM

Feb 14 2020

makarius committed rISABELLEe596ea18bf3e: Added tag Isabelle2020-RC0 for changeset 21c0b3a9d2f8.
Added tag Isabelle2020-RC0 for changeset 21c0b3a9d2f8
Feb 14 2020, 10:26 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2020.
Feb 14 2020, 10:02 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2020.
Feb 14 2020, 9:50 PM
makarius created Blog Post: Release Candidates for Isabelle2020.
Feb 14 2020, 9:43 PM
makarius updated the task description for T8: Clarify underlying Mercurial version.
Feb 14 2020, 9:30 PM · isabelle-release, phabricator-setup
makarius updated the task description for T8: Clarify underlying Mercurial version.
Feb 14 2020, 9:30 PM · isabelle-release, phabricator-setup
makarius updated the task description for T8: Clarify underlying Mercurial version.
Feb 14 2020, 9:30 PM · isabelle-release, phabricator-setup
makarius closed T8: Clarify underlying Mercurial version as Resolved.

Following Isabelle/8b0b8b9ea653, Mercurial 3.9.2 from 23-Sep-2016 is fine for now:

Feb 14 2020, 9:27 PM · isabelle-release, phabricator-setup
nipkow committed rAFP0a8ecf7a601e: fixed broken proofs.
fixed broken proofs
Feb 14 2020, 6:50 PM
nipkow committed rAFP474f409ebe72: fixed broken proof.
fixed broken proof
Feb 14 2020, 6:50 PM
nipkow committed rAFPe8d45180636f: merge from AFP 2019.
merge from AFP 2019
Feb 14 2020, 5:36 PM
pruvisto committed rAFP77a8004b99f4: sitegen for Arith_Prog_Rel_Primes.
sitegen for Arith_Prog_Rel_Primes
Feb 14 2020, 5:36 PM
nipkow committed rAFP6303a7ad1291: New entry Subset_Boolean_Algebras.
New entry Subset_Boolean_Algebras
Feb 14 2020, 5:36 PM
pruvisto committed rAFPbd5ff2d92ffa: new entry Arith_Prog_Rel_Primes.
new entry Arith_Prog_Rel_Primes
Feb 14 2020, 5:36 PM
paulson <lp15@cam.ac.uk> committed rAFP11ff77e058c4: webpage for Mersenne_Primes.
webpage for Mersenne_Primes
Feb 14 2020, 5:36 PM
pruvisto committed rAFPa222e106ac18: added new entries: Complex_Geometry and Poincare_Disc.
added new entries: Complex_Geometry and Poincare_Disc
Feb 14 2020, 5:36 PM
paulson <lp15@cam.ac.uk> committed rAFPcd30610ccf05: new entry Mersenne_Primes.
new entry Mersenne_Primes
Feb 14 2020, 5:36 PM
pruvisto committed rAFPa4ca8d95843b: fixed incorrect HTML entity in Poincare_Disc metadata.
fixed incorrect HTML entity in Poincare_Disc metadata
Feb 14 2020, 5:36 PM
pruvisto committed rAFP1775f91f0787: Fixed broken citation in Poincare_Disc.
Fixed broken citation in Poincare_Disc
Feb 14 2020, 5:36 PM
paulson <lp15@cam.ac.uk> committed rAFPc0d0d29ff0e7: Approximation_Algorithms website.
Approximation_Algorithms website
Feb 14 2020, 5:36 PM