Page MenuHomeIsabelle/Phabricator

Open Tasks

Normal (4)

Wishlist (3)

Recent Activity

Today

desharna committed rAFPd04de3d51efb: Fix failing proofs after update to Metis 2.4.
Fix failing proofs after update to Metis 2.4
Thu, Jul 9, 1:42 PM
desharna committed rISABELLE913162a47d9f: Update Metis to 2.4.
Update Metis to 2.4
Thu, Jul 9, 11:41 AM

Yesterday

makarius committed rISABELLEa7e6ac2dfa58: updated to polyml-5.8.1-20200708: recent repository version for testing;.
updated to polyml-5.8.1-20200708: recent repository version for testing;
Wed, Jul 8, 5:45 PM
makarius committed rISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true;.
more robust protocol for "Timing ..." messages, notably for pide_session=true;
Wed, Jul 8, 5:45 PM

Mon, Jul 6

blanchette committed rISABELLE3e08311ada8e: removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible….
removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible…
Mon, Jul 6, 4:53 PM
dcjm added a reverting change for rPOLYML744d14ffd49b: Fix bug found by Makarius in generated code. It seems to have been introduced…: rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings..
Mon, Jul 6, 3:26 PM
dcjm committed rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings. (authored by dcjm).
Convert single bindings from mutual recursion into simple bindings.
Mon, Jul 6, 3:26 PM
dcjm committed rPOLYMLa020d4b5f62b: The "setter" for a container refers to the container itself so any bindings… (authored by dcjm).
The "setter" for a container refers to the container itself so any bindings…
Mon, Jul 6, 3:26 PM
dcjm committed rPOLYMLade5d57318f0: Fix function name: they're mutual bindings not mutable. (authored by dcjm).
Fix function name: they're mutual bindings not mutable.
Mon, Jul 6, 3:26 PM
dcjm committed rPOLYMLd761f194071f: When analysing the usage pattern of a recursive function we need to consider… (authored by dcjm).
When analysing the usage pattern of a recursive function we need to consider…
Mon, Jul 6, 3:26 PM
dcjm committed rPOLYML7edf731ebd7f: Fix use of "print" rather than "stream" for debugging. (authored by dcjm).
Fix use of "print" rather than "stream" for debugging.
Mon, Jul 6, 3:26 PM
florian.haftmann committed rAFP1cdcce397e9d: separation of traditional bit operations.
separation of traditional bit operations
Mon, Jul 6, 1:04 PM
florian.haftmann committed rISABELLE379d0c207c29: separation of traditional bit operations.
separation of traditional bit operations
Mon, Jul 6, 1:03 PM

Sun, Jul 5

makarius committed rISABELLE720b72513ae5: no pide_session on macos: avoid odd "hang" of remote_build_history;.
no pide_session on macos: avoid odd "hang" of remote_build_history;
Sun, Jul 5, 11:23 AM
makarius committed rISABELLEf43b08980f56: support generated preferences, i.e. non-strict system options;.
support generated preferences, i.e. non-strict system options;
Sun, Jul 5, 11:23 AM
florian.haftmann committed rISABELLE4a013c92a091: factored out auxiliary theory.
factored out auxiliary theory
Sun, Jul 5, 8:04 AM
florian.haftmann committed rISABELLEc7ac6d4f3914: prefer explicit proof.
prefer explicit proof
Sun, Jul 5, 8:04 AM
florian.haftmann committed rAFPa03e9b5d8dc9: factored out auxiliary theory.
factored out auxiliary theory
Sun, Jul 5, 8:04 AM

Sat, Jul 4

Andreas Lochbihler committed rAFPb5b8255ae4c4: more operations for maps.
more operations for maps
Sat, Jul 4, 5:41 PM

Fri, Jul 3

makarius committed rISABELLEcb7ddc321f52: tuned whitespace;.
tuned whitespace;
Fri, Jul 3, 8:08 PM
makarius committed rISABELLE088e3aa85250: clarified signature;.
clarified signature;
Fri, Jul 3, 8:08 PM
makarius committed rISABELLEbbec0acf2592: use less memory on old hardware;.
use less memory on old hardware;
Fri, Jul 3, 8:08 PM
makarius committed rISABELLEc8c3f4f0f68b: clarified log message (more uniform);.
clarified log message (more uniform);
Fri, Jul 3, 8:08 PM
florian.haftmann committed rISABELLE8bff286878bf: misc lemma tuning.
misc lemma tuning
Fri, Jul 3, 12:11 PM
florian.haftmann committed rISABELLE66beb9d92e43: explicit proofs for bit projections.
explicit proofs for bit projections
Fri, Jul 3, 12:11 PM
florian.haftmann committed rAFPf90f9d593a88: misc lemma tuning.
misc lemma tuning
Fri, Jul 3, 12:10 PM

Thu, Jul 2

florian.haftmann committed rAFP81a8bf702c09: activated simproc defined_all.
activated simproc defined_all
Thu, Jul 2, 6:13 PM
florian.haftmann committed rISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-all.
extraction of equations x = t from premises beneath meta-all
Thu, Jul 2, 6:12 PM
florian.haftmann committed rAFPe0714a129570: updated documentation.
updated documentation
Thu, Jul 2, 4:29 PM
florian.haftmann committed rAFPb8a6808299e5: obsolete duplicates.
obsolete duplicates
Thu, Jul 2, 2:10 PM
florian.haftmann committed rISABELLEec17263ec38d: removed superfluous dependency.
removed superfluous dependency
Thu, Jul 2, 2:09 PM
florian.haftmann committed rISABELLEace45a11a45e: a small aggiornamento for Z2.
a small aggiornamento for Z2
Thu, Jul 2, 2:09 PM
florian.haftmann committed rAFP3ceb3fe8ab08: factored out ancient numeral representation.
factored out ancient numeral representation
Thu, Jul 2, 9:14 AM
florian.haftmann committed rAFP82e10d1ca9e1: moved to Word_Lib.
moved to Word_Lib
Thu, Jul 2, 9:14 AM
florian.haftmann committed rAFP04f54c116f30: tuned whitespace.
tuned whitespace
Thu, Jul 2, 9:14 AM
florian.haftmann committed rISABELLE76193dd4aec8: factored out ancient numeral representation.
factored out ancient numeral representation
Thu, Jul 2, 9:14 AM
florian.haftmann committed rISABELLEa1cf296a7786: moved to Word_Lib.
moved to Word_Lib
Thu, Jul 2, 9:14 AM
florian.haftmann committed rISABELLE10a8d943a8d8: more explicit proofs.
more explicit proofs
Thu, Jul 2, 9:14 AM

Wed, Jul 1

makarius committed rISABELLE694009ed4ee1: clarified options --- potentially more robust;.
clarified options --- potentially more robust;
Wed, Jul 1, 10:22 PM
makarius committed rISABELLEcea6087e8a70: tuned message;.
tuned message;
Wed, Jul 1, 10:05 PM