Page MenuHomeIsabelle/Phabricator
Feed All Stories

Jan 19 2020

makarius committed rISABELLE028edb1e5b99: clarified file names;.
clarified file names;
Jan 19 2020, 3:03 PM
makarius committed rISABELLEc1c61d0d8e7c: clarified build_polyml_component: include IDE entry point for ML compiler;.
clarified build_polyml_component: include IDE entry point for ML compiler;
Jan 19 2020, 3:03 PM
makarius committed rISABELLEd7f8ee80ad42: merged.
merged
Jan 19 2020, 3:03 PM
makarius committed rISABELLE933ad2385480: tuned spelling;.
tuned spelling;
Jan 19 2020, 3:03 PM
traytel committed rISABELLEfce780f9c9c6: new examples of BNF lifting across quotients using a new theory of confluence,.
new examples of BNF lifting across quotients using a new theory of confluence,
Jan 19 2020, 11:15 AM
dcjm committed rPOLYML5237b653aa69: Rename Root.ML to avoid possible conflict with ROOT.ML in Isabelle. (authored by dcjm).
Rename Root.ML to avoid possible conflict with ROOT.ML in Isabelle.
Jan 19 2020, 9:12 AM

Jan 18 2020

dcjm committed rPOLYMLf5b8283a1a19: Remove unused variable. This should have been removed in commit 889f7c37. (authored by dcjm).
Remove unused variable. This should have been removed in commit 889f7c37.
Jan 18 2020, 6:53 PM
dcjm committed rPOLYMLabb79876106c: Fix case problem in one entry. (authored by dcjm).
Fix case problem in one entry.
Jan 18 2020, 6:53 PM

Jan 17 2020

pruvisto committed rISABELLEa3f7f00b4fd8: Removed unnecessary and problematic trivial lemma from HOL-Algebra.
Removed unnecessary and problematic trivial lemma from HOL-Algebra
Jan 17 2020, 10:26 PM

Jan 16 2020

makarius committed rISABELLE5556ae257df9: proper executable file;.
proper executable file;
Jan 16 2020, 5:05 PM
makarius committed rISABELLE5e7ba6aa85d7: more documentation: odd option for special situations;.
more documentation: odd option for special situations;
Jan 16 2020, 4:42 PM
makarius committed rISABELLE21995f5e8126: tuned;.
tuned;
Jan 16 2020, 4:42 PM
makarius committed rISABELLE57861bd0a3e1: updated to sumatra_pdf-3.1.2-1: x86_64-windows;.
updated to sumatra_pdf-3.1.2-1: x86_64-windows;
Jan 16 2020, 4:29 PM
makarius triaged T11: HOL-Quickcheck_Examples fails on Windows as Low priority.
Jan 16 2020, 4:07 PM
makarius committed rISABELLEb3b992f6ad8f: updated to stack-2.1.3, stackage lts-13.19, ghc-8.6.4;.
updated to stack-2.1.3, stackage lts-13.19, ghc-8.6.4;
Jan 16 2020, 4:06 PM
makarius committed rISABELLE7e8e5e1f8f90: updated to opam-2.0.6;.
updated to opam-2.0.6;
Jan 16 2020, 4:06 PM
makarius committed rISABELLE06bb82e7af2a: updated to current cygwin, after 3.1.2-1 from 21-Dec-2019;.
updated to current cygwin, after 3.1.2-1 from 21-Dec-2019;
Jan 16 2020, 4:06 PM
makarius triaged T10: Font rendering quality in OpenJDK 11 vs. 17 as Low priority.
Jan 16 2020, 12:08 PM

Jan 15 2020

makarius committed rISABELLE0243bf758e79: updated to jdk-11.0.6+10;.
updated to jdk-11.0.6+10;
Jan 15 2020, 8:53 PM
makarius committed rISABELLE8313dca6dee9: misc tuning, following hint by IntelliJ;.
misc tuning, following hint by IntelliJ;
Jan 15 2020, 8:53 PM
makarius committed rISABELLE6316debd3a9f: tuned;.
tuned;
Jan 15 2020, 8:53 PM
makarius committed rISABELLEb9ea2467c929: tuned -- avoid deprecated constructors;.
tuned -- avoid deprecated constructors;
Jan 15 2020, 8:53 PM
makarius committed rISABELLE942cc80ba18a: unused -- clone of Option.apply;.
unused -- clone of Option.apply;
Jan 15 2020, 8:53 PM
makarius committed rISABELLE5965e6e3c3ec: proper comparison of Option values, following hint by IntelliJ;.
proper comparison of Option values, following hint by IntelliJ;
Jan 15 2020, 8:53 PM
makarius created Blog Post: Command-line tool "isabelle scala_project".
Jan 15 2020, 3:34 PM
makarius committed rISABELLE820cf124dced: added "isabelle scala_project" to support e.g. IntelliJ IDEA;.
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
Jan 15 2020, 3:30 PM
makarius committed rISABELLEe40f287c25c4: unused;.
unused;
Jan 15 2020, 3:30 PM

Jan 14 2020

makarius committed rISABELLE26801434d628: more antiquotations;.
more antiquotations;
Jan 14 2020, 4:21 PM

Jan 13 2020

makarius committed rISABELLE5ccf60c1f47c: tuned messages;.
tuned messages;
Jan 13 2020, 9:43 PM
makarius committed rISABELLE7832d912d950: tuned;.
tuned;
Jan 13 2020, 9:43 PM
makarius committed rISABELLE201486ced92d: clarified output channel;.
clarified output channel;
Jan 13 2020, 9:43 PM
makarius committed rISABELLE85274743f789: clarified option -f: avoid accidental target_clean for proper release snapshot;.
clarified option -f: avoid accidental target_clean for proper release snapshot;
Jan 13 2020, 9:43 PM
makarius added a comment to T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.

See also https://matrix.org "An open network for secure, decentralized communication"

Jan 13 2020, 2:24 PM
makarius added a member for isabelle-repository: peter_lammich.
Jan 13 2020, 11:50 AM

Jan 12 2020

makarius committed rISABELLE1c4ec697bee5: more robust;.
more robust;
Jan 12 2020, 11:30 PM
makarius committed rISABELLEb05aca9cee75: updated to sqlite-jdbc-3.30.1;.
updated to sqlite-jdbc-3.30.1;
Jan 12 2020, 11:30 PM
makarius committed rISABELLE897ff7e68a10: updated to postgresql-42.2.9;.
updated to postgresql-42.2.9;
Jan 12 2020, 11:30 PM
makarius committed rISABELLEfd5cd1daf6a9: build in $ISABELLE_HOME;.
build in $ISABELLE_HOME;
Jan 12 2020, 9:53 PM
makarius committed rISABELLE91d5a8255c98: build in $ISABELLE_HOME;.
build in $ISABELLE_HOME;
Jan 12 2020, 9:53 PM
makarius committed rISABELLEf0581273bd7b: clarified fresh build;.
clarified fresh build;
Jan 12 2020, 9:53 PM
makarius updated the task description for T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.
Jan 12 2020, 4:19 PM
makarius updated the task description for T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.
Jan 12 2020, 4:18 PM
makarius updated the task description for T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.
Jan 12 2020, 4:18 PM
makarius triaged T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow as Low priority.
Jan 12 2020, 4:14 PM
makarius added a comment to T3: Adapt Isabelle/VSCode to Webview API.

Here is a proposed change:

# HG changeset patch
# User XYZ
# Date 1573057691 -3600
#      Wed Nov 06 17:28:11 2019 +0100
# Node ID ec7c536b2b7ab516541f31e5a5be93d7391c27a1
# Parent  b3956a37c99476571bfda9312da927dfdfdcb6b1
replaced previewHtml with WebviewPanel
Jan 12 2020, 4:10 PM · isabelle-release
makarius added a project to T8: Clarify underlying Mercurial version: phabricator-setup.
Jan 12 2020, 4:06 PM · isabelle-release, phabricator-setup
makarius claimed T8: Clarify underlying Mercurial version.
Jan 12 2020, 4:05 PM · isabelle-release, phabricator-setup
makarius triaged T8: Clarify underlying Mercurial version as Low priority.
Jan 12 2020, 3:50 PM · isabelle-release, phabricator-setup

Jan 11 2020

makarius committed rISABELLE462f341407b4: tuned documentation;.
tuned documentation;
Jan 11 2020, 4:22 PM
makarius committed rISABELLEaecea7c4bda1: tuned;.
tuned;
Jan 11 2020, 3:58 PM

Jan 10 2020

makarius committed rISABELLEce3409dfb18c: clarified script name;.
clarified script name;
Jan 10 2020, 5:21 PM
makarius added a comment to rISABELLE597059a44d6f: prefer mercurial-2.8.2 for more robustness (i.e. the version used by the….
Jan 10 2020, 4:07 PM
makarius added a comment to rISABELLE597059a44d6f: prefer mercurial-2.8.2 for more robustness (i.e. the version used by the….

See also https://discourse.phabricator-community.org/t/prefer-old-mercurial-2-8-2-to-avoid-various-problems/3431

Jan 10 2020, 4:03 PM
makarius committed rISABELLE597059a44d6f: prefer mercurial-2.8.2 for more robustness (i.e. the version used by the….
prefer mercurial-2.8.2 for more robustness (i.e. the version used by the…
Jan 10 2020, 3:54 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP3d850b1af9cd: small adjustments for new implementation.
small adjustments for new implementation
Jan 10 2020, 11:40 AM
Julian Brunner <julianbrunner@gmail.com> committed rAFPfbd84ab865a3: improved emptiness check implementation and added more translation ideas.
improved emptiness check implementation and added more translation ideas
Jan 10 2020, 11:40 AM

Jan 9 2020

makarius committed rISABELLEfcf5ee85743d: more Isabelle fonts, notably for File Browser title in GTK L&F;.
more Isabelle fonts, notably for File Browser title in GTK L&F;
Jan 9 2020, 5:03 PM
makarius committed rISABELLE21a41356d78f: proper name;.
proper name;
Jan 9 2020, 5:03 PM
makarius committed rISABELLE411c0322c09d: eliminated deprecated scala.collection.JavaConversions;.
eliminated deprecated scala.collection.JavaConversions;
Jan 9 2020, 5:03 PM
makarius committed rISABELLEec48da635e6c: unused;.
unused;
Jan 9 2020, 5:03 PM
makarius committed rISABELLE7f2cd237ee4f: tuned -- more direct java.util.Map.of;.
tuned -- more direct java.util.Map.of;
Jan 9 2020, 5:03 PM
nipkow committed rISABELLEce45299cce44: added lemma.
added lemma
Jan 9 2020, 10:15 AM

Jan 7 2020

traytel committed rISABELLE15c6f253b9f3: merged.
merged
Jan 7 2020, 5:13 PM
traytel committed rISABELLEc71a44893645: eliminated one redundant proof obligation in lift_bnf for quotients.
eliminated one redundant proof obligation in lift_bnf for quotients
Jan 7 2020, 5:13 PM
blanchette committed rISABELLE475b2260b9c4: removed experimental option to SPASS.
removed experimental option to SPASS
Jan 7 2020, 4:33 PM
Andreas Halkjær From <s144442@student.dtu.dk> committed rAFPb504f070987b: Restrict the GoTo rule.
Restrict the GoTo rule
Jan 7 2020, 2:15 PM
nipkow committed rISABELLE41f3ca717da5: alternative deletion in Red-Black trees.
alternative deletion in Red-Black trees
Jan 7 2020, 12:37 PM
nipkow committed rISABELLEb3a93a91803b: generalized thm (as suggested by Christian Weinz).
generalized thm (as suggested by Christian Weinz)
Jan 7 2020, 8:47 AM
nipkow committed rISABELLEcd0b0717c4e4: tunded.
tunded
Jan 7 2020, 6:54 AM
kleing committed rAFP8d4d754b2196: adapt to isabelle fb788bd799d9.
adapt to isabelle fb788bd799d9
Jan 7 2020, 2:16 AM
kleing committed rAFP7f9a5c0cfaa1: merge from afp-2019.
merge from afp-2019
Jan 7 2020, 1:50 AM
kleing committed rAFPc2a5fad2fd66: new entry Hybrid_Logic.
new entry Hybrid_Logic
Jan 7 2020, 1:50 AM
nipkow committed rAFPdcbd8cc33205: New entry Zeta_3_Irrational.
New entry Zeta_3_Irrational
Jan 7 2020, 1:50 AM

Jan 2 2020

pruvisto committed rAFP3c6cf3b9146b: More material for Zeta_Function: Hadjicostas's formula.
More material for Zeta_Function: Hadjicostas's formula
Jan 2 2020, 7:16 PM

Dec 28 2019

nipkow committed rISABELLEfb788bd799d9: tuned.
tuned
Dec 28 2019, 11:45 PM
nipkow committed rISABELLE857453c0db3d: tuned.
tuned
Dec 28 2019, 12:16 AM

Dec 27 2019

makarius committed rISABELLE3c4c171344f4: more examples;.
more examples;
Dec 27 2019, 4:22 PM
Frédéric Tuong committed rAFPc9b532b32acc: synchronize with isabelle_c/a8ec2f73aa2426b34f6c7548f720abd31413ca79 , update….
synchronize with isabelle_c/a8ec2f73aa2426b34f6c7548f720abd31413ca79 , update…
Dec 27 2019, 2:27 PM
nipkow committed rISABELLE7a0a6c56015e: tuned.
tuned
Dec 27 2019, 10:59 AM

Dec 26 2019

makarius committed rAFPd4df5c37f780: tuned timeout;.
tuned timeout;
Dec 26 2019, 9:56 PM
makarius committed rAFP1531e2d56482: tuned timeout;.
tuned timeout;
Dec 26 2019, 9:00 PM

Dec 24 2019

nipkow committed rISABELLEa956b769903e: tuned.
tuned
Dec 24 2019, 9:51 PM

Dec 23 2019

makarius committed rISABELLEee9998bb417b: tuned;.
tuned;
Dec 23 2019, 11:02 PM
makarius committed rISABELLE7a53175fb0f4: NEWS;.
NEWS;
Dec 23 2019, 11:02 PM
makarius committed rISABELLEd72d4a9316c9: updated platform situation: 32bit variants are marginal or absent;.
updated platform situation: 32bit variants are marginal or absent;
Dec 23 2019, 11:02 PM
makarius committed rISABELLEdfc52eb97ff4: repackage as csdp-6.1-1, with proper platform names;.
repackage as csdp-6.1-1, with proper platform names;
Dec 23 2019, 11:02 PM
makarius committed rISABELLE6d9dd5309b85: proper File.platform_path for Windows;.
proper File.platform_path for Windows;
Dec 23 2019, 9:43 PM
makarius committed rISABELLE05400628c56b: updated csdp-6.1: Linux and Windows executables are as before, but macOS has….
updated csdp-6.1: Linux and Windows executables are as before, but macOS has…
Dec 23 2019, 9:43 PM
makarius committed rISABELLE373dcdd363dc: updated linux_app-20191223: x86_64-linux;.
updated linux_app-20191223: x86_64-linux;
Dec 23 2019, 9:43 PM
immler committed rAFPdf45a67089ff: remove carriage return.
remove carriage return
Dec 23 2019, 12:44 AM

Dec 22 2019

makarius changed the Default View Policy policy for application Spaces from All Users to Public (No Login Required).
Dec 22 2019, 6:35 PM
makarius changed the Default View Policy policy for application Slowvote from All Users to Public (No Login Required).
Dec 22 2019, 6:34 PM
makarius changed the Default View Policy policy for application Paste from All Users to Public (No Login Required).
Dec 22 2019, 6:33 PM
makarius changed the Default View Policy policy for application Owners from All Users to Public (No Login Required).
Dec 22 2019, 6:33 PM
makarius changed the Can Manage Macros policy for application Macro from All Users to Administrators.
Dec 22 2019, 6:32 PM
makarius changed the Can Create Documents policy for application Legalpad from All Users to Administrators.
Dec 22 2019, 6:32 PM
makarius changed the Default Build Plan View Policy policy for application Harbormaster from All Users to Public (No Login Required).
Dec 22 2019, 6:31 PM
makarius changed the Default View Policy policy for application Files from All Users to Public (No Login Required).
Dec 22 2019, 6:31 PM
makarius changed the Default View Policy policy for application Diviner from All Users to Public (No Login Required).
Dec 22 2019, 6:28 PM
makarius changed the Default View Policy policy for application Pholio from All Users to Public (No Login Required).
Dec 22 2019, 6:27 PM