Page MenuHomeIsabelle/Phabricator
Feed All Stories

Sun, Jan 19

makarius committed rISABELLE028edb1e5b99: clarified file names;.
clarified file names;
Sun, Jan 19, 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;
Sun, Jan 19, 3:03 PM
makarius committed rISABELLEd7f8ee80ad42: merged.
merged
Sun, Jan 19, 3:03 PM
makarius committed rISABELLE933ad2385480: tuned spelling;.
tuned spelling;
Sun, Jan 19, 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,
Sun, Jan 19, 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.
Sun, Jan 19, 9:12 AM

Sat, Jan 18

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.
Sat, Jan 18, 6:53 PM
dcjm committed rPOLYMLabb79876106c: Fix case problem in one entry. (authored by dcjm).
Fix case problem in one entry.
Sat, Jan 18, 6:53 PM

Fri, Jan 17

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

Thu, Jan 16

makarius committed rISABELLE5556ae257df9: proper executable file;.
proper executable file;
Thu, Jan 16, 5:05 PM
makarius committed rISABELLE5e7ba6aa85d7: more documentation: odd option for special situations;.
more documentation: odd option for special situations;
Thu, Jan 16, 4:42 PM
makarius committed rISABELLE21995f5e8126: tuned;.
tuned;
Thu, Jan 16, 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;
Thu, Jan 16, 4:29 PM
makarius triaged T11: HOL-Quickcheck_Examples fails on Windows as Low priority.
Thu, Jan 16, 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;
Thu, Jan 16, 4:06 PM
makarius committed rISABELLE7e8e5e1f8f90: updated to opam-2.0.6;.
updated to opam-2.0.6;
Thu, Jan 16, 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;
Thu, Jan 16, 4:06 PM
makarius triaged T10: Font rendering quality in OpenJDK 11 vs. 13 as Low priority.
Thu, Jan 16, 12:08 PM

Wed, Jan 15

makarius committed rISABELLE0243bf758e79: updated to jdk-11.0.6+10;.
updated to jdk-11.0.6+10;
Wed, Jan 15, 8:53 PM
makarius committed rISABELLE8313dca6dee9: misc tuning, following hint by IntelliJ;.
misc tuning, following hint by IntelliJ;
Wed, Jan 15, 8:53 PM
makarius committed rISABELLE6316debd3a9f: tuned;.
tuned;
Wed, Jan 15, 8:53 PM
makarius committed rISABELLEb9ea2467c929: tuned -- avoid deprecated constructors;.
tuned -- avoid deprecated constructors;
Wed, Jan 15, 8:53 PM
makarius committed rISABELLE942cc80ba18a: unused -- clone of Option.apply;.
unused -- clone of Option.apply;
Wed, Jan 15, 8:53 PM
makarius committed rISABELLE5965e6e3c3ec: proper comparison of Option values, following hint by IntelliJ;.
proper comparison of Option values, following hint by IntelliJ;
Wed, Jan 15, 8:53 PM
makarius created Blog Post: Command-line tool "isabelle scala_project".
Wed, Jan 15, 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;
Wed, Jan 15, 3:30 PM
makarius committed rISABELLEe40f287c25c4: unused;.
unused;
Wed, Jan 15, 3:30 PM

Tue, Jan 14

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

Mon, Jan 13

makarius committed rISABELLE5ccf60c1f47c: tuned messages;.
tuned messages;
Mon, Jan 13, 9:43 PM
makarius committed rISABELLE7832d912d950: tuned;.
tuned;
Mon, Jan 13, 9:43 PM
makarius committed rISABELLE201486ced92d: clarified output channel;.
clarified output channel;
Mon, Jan 13, 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;
Mon, Jan 13, 9:43 PM
makarius added a comment to T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow, zulip.

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

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

Sun, Jan 12

makarius committed rISABELLE1c4ec697bee5: more robust;.
more robust;
Sun, Jan 12, 11:30 PM
makarius committed rISABELLEb05aca9cee75: updated to sqlite-jdbc-3.30.1;.
updated to sqlite-jdbc-3.30.1;
Sun, Jan 12, 11:30 PM
makarius committed rISABELLE897ff7e68a10: updated to postgresql-42.2.9;.
updated to postgresql-42.2.9;
Sun, Jan 12, 11:30 PM
makarius committed rISABELLEfd5cd1daf6a9: build in $ISABELLE_HOME;.
build in $ISABELLE_HOME;
Sun, Jan 12, 9:53 PM
makarius committed rISABELLE91d5a8255c98: build in $ISABELLE_HOME;.
build in $ISABELLE_HOME;
Sun, Jan 12, 9:53 PM
makarius committed rISABELLEf0581273bd7b: clarified fresh build;.
clarified fresh build;
Sun, Jan 12, 9:53 PM
makarius updated the task description for T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow, zulip.
Sun, Jan 12, 4:19 PM
makarius updated the task description for T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow, zulip.
Sun, Jan 12, 4:18 PM
makarius updated the task description for T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow, zulip.
Sun, Jan 12, 4:18 PM
makarius triaged T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow, zulip as Low priority.
Sun, Jan 12, 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
Sun, Jan 12, 4:10 PM
makarius added a project to T8: Clarify underlying Mercurial version: phabricator-setup.
Sun, Jan 12, 4:06 PM · phabricator-setup
makarius claimed T8: Clarify underlying Mercurial version.
Sun, Jan 12, 4:05 PM · phabricator-setup
makarius triaged T8: Clarify underlying Mercurial version as Low priority.
Sun, Jan 12, 3:50 PM · phabricator-setup

Sat, Jan 11

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

Fri, Jan 10

makarius committed rISABELLEce3409dfb18c: clarified script name;.
clarified script name;
Fri, Jan 10, 5:21 PM
makarius added a comment to rISABELLE597059a44d6f: prefer mercurial-2.8.2 for more robustness (i.e. the version used by the….
Fri, Jan 10, 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

Fri, Jan 10, 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…
Fri, Jan 10, 3:54 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP3d850b1af9cd: small adjustments for new implementation.
small adjustments for new implementation
Fri, Jan 10, 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
Fri, Jan 10, 11:40 AM

Thu, Jan 9

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;
Thu, Jan 9, 5:03 PM
makarius committed rISABELLE21a41356d78f: proper name;.
proper name;
Thu, Jan 9, 5:03 PM
makarius committed rISABELLE411c0322c09d: eliminated deprecated scala.collection.JavaConversions;.
eliminated deprecated scala.collection.JavaConversions;
Thu, Jan 9, 5:03 PM
makarius committed rISABELLEec48da635e6c: unused;.
unused;
Thu, Jan 9, 5:03 PM
makarius committed rISABELLE7f2cd237ee4f: tuned -- more direct java.util.Map.of;.
tuned -- more direct java.util.Map.of;
Thu, Jan 9, 5:03 PM
nipkow committed rISABELLEce45299cce44: added lemma.
added lemma
Thu, Jan 9, 10:15 AM

Tue, Jan 7

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

Thu, Jan 2

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

Sat, Dec 28

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

Fri, Dec 27

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

Thu, Dec 26

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

Tue, Dec 24

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

Mon, Dec 23

makarius committed rISABELLEee9998bb417b: tuned;.
tuned;
Mon, Dec 23, 11:02 PM
makarius committed rISABELLE7a53175fb0f4: NEWS;.
NEWS;
Mon, Dec 23, 11:02 PM
makarius committed rISABELLEd72d4a9316c9: updated platform situation: 32bit variants are marginal or absent;.
updated platform situation: 32bit variants are marginal or absent;
Mon, Dec 23, 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;
Mon, Dec 23, 11:02 PM
makarius committed rISABELLE6d9dd5309b85: proper File.platform_path for Windows;.
proper File.platform_path for Windows;
Mon, Dec 23, 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…
Mon, Dec 23, 9:43 PM
makarius committed rISABELLE373dcdd363dc: updated linux_app-20191223: x86_64-linux;.
updated linux_app-20191223: x86_64-linux;
Mon, Dec 23, 9:43 PM
immler committed rAFPdf45a67089ff: remove carriage return.
remove carriage return
Mon, Dec 23, 12:44 AM

Sun, Dec 22

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