Page MenuHomeIsabelle/Phabricator
Feed All Stories

Yesterday

desharna committed rAFPb335908ca5ac: merged.
merged
Tue, Dec 7, 12:07 PM
desharna committed rAFP1cdb95bf9f7c: generalized standard formula redundancy out of standard redundancy.
generalized standard formula redundancy out of standard redundancy
Tue, Dec 7, 12:07 PM
makarius committed rAFP5284bc2e2dfb: discontinued Parse.text;.
discontinued Parse.text;
Tue, Dec 7, 12:12 AM
makarius committed rAFPc2061c79823c: merged.
merged
Tue, Dec 7, 12:12 AM
makarius committed rAFP2fdd87fc6dd7: discontinued old-style {* verbatim *} tokens;.
discontinued old-style {* verbatim *} tokens;
Tue, Dec 7, 12:12 AM
makarius committed rISABELLEfa5476c54731: tuned proof;.
tuned proof;
Tue, Dec 7, 12:12 AM
makarius committed rISABELLE56247fdb8bbb: discontinued old-style {* verbatim *} tokens;.
discontinued old-style {* verbatim *} tokens;
Tue, Dec 7, 12:12 AM
makarius committed rISABELLE2df334453c4c: isabelle update_cartouches;.
isabelle update_cartouches;
Tue, Dec 7, 12:12 AM

Mon, Dec 6

desharna committed rAFP90f5fb60422f: weakened locale assumptions: wfP implies asymp.
weakened locale assumptions: wfP implies asymp
Mon, Dec 6, 9:41 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP7c1a5a8e9959: Add papers to metadata..
Add papers to metadata.
Mon, Dec 6, 5:06 PM
desharna committed rAFP4c46cf956c77: refactored Standard_Redundancy_Criterion to not use ordering type classes.
refactored Standard_Redundancy_Criterion to not use ordering type classes
Mon, Dec 6, 1:25 PM
makarius committed rAFP1ffda7071d4a: isabelle update_cartouches;.
isabelle update_cartouches;
Mon, Dec 6, 1:06 PM
makarius committed rAFPd4ed7c4aca73: removed obsolete "extend" operation;.
removed obsolete "extend" operation;
Mon, Dec 6, 12:21 PM

Sun, Dec 5

makarius committed rAFP98ecfb2297ef: more symbolic latex_output via XML (using YXML within text);.
more symbolic latex_output via XML (using YXML within text);
Sun, Dec 5, 9:04 PM
makarius committed rISABELLE229d7ea628c2: more symbolic latex_output via XML (using YXML within text);.
more symbolic latex_output via XML (using YXML within text);
Sun, Dec 5, 9:04 PM
makarius committed rISABELLEf32ac01aef5e: tuned signature: remove unused;.
tuned signature: remove unused;
Sun, Dec 5, 9:04 PM
makarius committed rISABELLE947bb3e09a88: prefer symbolic Latex.environment (typeset in Isabelle/Scala);.
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
Sun, Dec 5, 9:04 PM
makarius committed rISABELLE944d4d616ca0: clarified corner cases of syntax;.
clarified corner cases of syntax;
Sun, Dec 5, 9:04 PM
makarius committed rISABELLE1e84ae3e886e: tuned signature;.
tuned signature;
Sun, Dec 5, 9:04 PM
makarius committed rISABELLE89c7f74b5ae1: clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);.
clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
Sun, Dec 5, 9:04 PM
makarius committed rAFPdf2034347bc9: prefer symbolic Latex.environment (typeset in Isabelle/Scala);.
prefer symbolic Latex.environment (typeset in Isabelle/Scala);
Sun, Dec 5, 4:37 PM
makarius committed rAFP0bc1235e5fb6: tuned signature;.
tuned signature;
Sun, Dec 5, 4:37 PM

Sat, Dec 4

makarius updated the post content for Blog Post: Release Candidates for Isabelle2021-1.
Sat, Dec 4, 11:10 PM
makarius committed rWEBSITE256393a9a400: only Windows 10 is tested;.
only Windows 10 is tested;
Sat, Dec 4, 10:36 PM
paulson <lp15@cam.ac.uk> committed rISABELLE0263787a06b4: a slightly simpler proof.
a slightly simpler proof
Sat, Dec 4, 9:30 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2021-1.
Sat, Dec 4, 9:22 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2021-1.
Sat, Dec 4, 8:16 PM
dcjm committed rPOLYML59bc13986b41: Update config.guess and config.sub from automake-1.16.3. For some reason… (authored by dcjm).
Update config.guess and config.sub from automake-1.16.3. For some reason…
Sat, Dec 4, 5:44 PM
makarius committed rISABELLE1a5d4586b6b0: provide component naproche-2d99afe5c349;.
provide component naproche-2d99afe5c349;
Sat, Dec 4, 5:31 PM
kappelmann committed rAFP5a8b07a912c1: feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics….
feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics…
Sat, Dec 4, 2:38 PM
makarius committed rISABELLEe8935405f082: merged.
merged
Sat, Dec 4, 1:25 PM
makarius committed rISABELLE98d2b3375258: Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2.
Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2
Sat, Dec 4, 1:25 PM
makarius committed rISABELLE8baf2e8b16e2: more documentation about Type/Const antiquotations;.
more documentation about Type/Const antiquotations;
Sat, Dec 4, 1:25 PM
makarius committed rISABELLE0ab2ed1489eb: more documentation about document build options;.
more documentation about document build options;
Sat, Dec 4, 1:25 PM
makarius committed rISABELLE0597884e6e91: tuned --- fewer IDE warnings;.
tuned --- fewer IDE warnings;
Sat, Dec 4, 1:25 PM
makarius committed rISABELLE9e9a308562da: address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of….
address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of…
Sat, Dec 4, 1:25 PM
makarius committed rISABELLEd54b3c96ee50: more robust physical timeout (despite 1bea05713dde), especially relevant for….
more robust physical timeout (despite 1bea05713dde), especially relevant for…
Sat, Dec 4, 1:25 PM

Fri, Dec 3

dcjm committed rPOLYMLcae32f905095: Update config.sub and config.guess and include a script to do this in the… (authored by dcjm).
Update config.sub and config.guess and include a script to do this in the…
Fri, Dec 3, 6:34 PM
dcjm committed rPOLYMLdced04294bb2: Check for presence of Mach-O relocation files and only include them if they're (authored by dcjm).
Check for presence of Mach-O relocation files and only include them if they're
Fri, Dec 3, 6:34 PM
dcjm committed rPOLYMLa63f2196a5e7: Fix incorrect argument when printing byte code assembly code. (authored by dcjm).
Fix incorrect argument when printing byte code assembly code.
Fri, Dec 3, 6:34 PM

Thu, Dec 2

Asta Halkjær From <andro.from@gmail.com> committed rAFPa2b90cb55ad1: Tuned: use a star in witness..
Tuned: use a star in witness.
Thu, Dec 2, 3:15 PM
kleing committed rAFP8dfc109e1ef5: merge from afp-2021-1.
merge from afp-2021-1
Thu, Dec 2, 8:14 AM
kleing committed rAFP001657f3e9b5: adjust for new tags in Isabelle2021-1-RC4.
adjust for new tags in Isabelle2021-1-RC4
Thu, Dec 2, 8:14 AM
Simon Wimmer <wimmers@in.tum.de> committed rAFP4cabc8dd3298: fix dangerous context management.
fix dangerous context management
Thu, Dec 2, 8:14 AM

Wed, Dec 1

paulson <lp15@cam.ac.uk> committed rAFP3232fddb53c7: In the definition of regular pair, switched from strict to non-strict.
In the definition of regular pair, switched from strict to non-strict
Wed, Dec 1, 8:11 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP068616f9fbde: Rename H to S in maximal_exactly_one..
Rename H to S in maximal_exactly_one.
Wed, Dec 1, 7:05 PM
Fabian Huch <huch@in.tum.de> committed rAFPb30cbcc1846c: tuned;.
tuned;
Wed, Dec 1, 5:40 PM
Fabian Huch <huch@in.tum.de> committed rAFP1266c86cf47b: added loader;.
added loader;
Wed, Dec 1, 5:40 PM
Fabian Huch <huch@in.tum.de> committed rAFPb32649b547e9: proper loading of foundational hrefs;.
proper loading of foundational hrefs;
Wed, Dec 1, 5:40 PM
Fabian Huch <huch@in.tum.de> committed rAFPd6ff995cf5a9: tuned: more canonical Isabelle code style;.
tuned: more canonical Isabelle code style;
Wed, Dec 1, 5:40 PM
Fabian Huch <huch@in.tum.de> committed rAFP53e6f3897fff: fix dependencies;.
fix dependencies;
Wed, Dec 1, 5:40 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFPad7234dfa6b4: Get rid of the sat abbreviation..
Get rid of the sat abbreviation.
Wed, Dec 1, 5:21 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP2f55c21c3d3d: Add missing spaces in semantics_tm..
Add missing spaces in semantics_tm.
Wed, Dec 1, 4:38 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP5dcf43ecbb6d: Non-conflicting name for boolean denotation..
Non-conflicting name for boolean denotation.
Wed, Dec 1, 4:16 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP9c5a5af856b8: No space in front of object-logic forall..
No space in front of object-logic forall.
Wed, Dec 1, 4:16 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFPbd0387cbded7: Simpler Hintikka definition..
Simpler Hintikka definition.
Wed, Dec 1, 4:16 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP7ed432999588: Add syntactic abbreviation for constants..
Add syntactic abbreviation for constants.
Wed, Dec 1, 4:16 PM
Fabian Huch <huch@in.tum.de> committed rAFPab1cf8fca876: added devel flag;.
added devel flag;
Wed, Dec 1, 11:10 AM
Fabian Huch <huch@in.tum.de> committed rAFPcc835fde7a38: updated about page;.
updated about page;
Wed, Dec 1, 11:10 AM

Tue, Nov 30

makarius added a comment to T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.

Flarum https://flarum.org looks like a pretty good alternative to Discourse, Matrix, Zulip etc.

Tue, Nov 30, 5:03 PM

Mon, Nov 29

desharna committed rISABELLE7b0a241732c1: added definitions multp{DM,HO} and corresponding lemmas.
added definitions multp{DM,HO} and corresponding lemmas
Mon, Nov 29, 1:34 PM
desharna committed rISABELLE2741ef11ccf6: added wfP_less to wellorder and wfP_less_multiset.
added wfP_less to wellorder and wfP_less_multiset
Mon, Nov 29, 1:34 PM

Sun, Nov 28

desharna committed rAFPc6cf7b096b98: fixed lemma following Isabelle/c256bba593f3.
fixed lemma following Isabelle/c256bba593f3
Sun, Nov 28, 4:34 PM
desharna committed rISABELLE4220dcd6c22e: restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3.
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
Sun, Nov 28, 2:17 PM

Sat, Nov 27

desharna committed rISABELLEa8927420a48b: merged.
merged
Sat, Nov 27, 10:21 PM
desharna committed rISABELLEc256bba593f3: redefined less_multiset to be based on multp.
redefined less_multiset to be based on multp
Sat, Nov 27, 10:21 PM
desharna committed rISABELLE691131ce4641: added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp.
added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp
Sat, Nov 27, 10:21 PM
desharna committed rISABELLEb5031a8f7718: added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to….
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to…
Sat, Nov 27, 10:21 PM
desharna committed rISABELLEaa51e974b688: added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max.
added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max
Sat, Nov 27, 10:21 PM
desharna committed rISABELLE74ac414618e2: added lemmas multp_implies_one_step, one_step_implies_multp, and….
added lemmas multp_implies_one_step, one_step_implies_multp, and…
Sat, Nov 27, 10:21 PM
desharna committed rISABELLE3e55e47a37e7: added lemma wfP_multp.
added lemma wfP_multp
Sat, Nov 27, 10:21 PM
desharna committed rISABELLE250ab1334309: added lemma mono_multp.
added lemma mono_multp
Sat, Nov 27, 10:21 PM
desharna committed rISABELLEc5059f9fbfba: added Multiset.multp as predicate equivalent of Multiset.mult.
added Multiset.multp as predicate equivalent of Multiset.mult
Sat, Nov 27, 10:21 PM
makarius committed rISABELLE25e9e7088561: address problems with launch4j and jdk-17 (see also 41d009462d3c);.
address problems with launch4j and jdk-17 (see also 41d009462d3c);
Sat, Nov 27, 6:48 PM
makarius committed rISABELLEae7912a42b9d: more robust build on midrange hardware;.
more robust build on midrange hardware;
Sat, Nov 27, 3:47 PM
makarius committed rISABELLEa5eb407ec867: clarified tests: omit somewhat pointless (unstable) results;.
clarified tests: omit somewhat pointless (unstable) results;
Sat, Nov 27, 3:47 PM
makarius committed rISABELLE014141670774: proper fields for gnuplot (amending b614e3e4146a);.
proper fields for gnuplot (amending b614e3e4146a);
Sat, Nov 27, 3:47 PM
makarius committed rISABELLE7420a7ac1a4c: tuned output;.
tuned output;
Sat, Nov 27, 3:47 PM
makarius committed rISABELLE204273f3a30e: tuned;.
tuned;
Sat, Nov 27, 3:47 PM
makarius added a comment to T29: Update component for Z3.

See also 796ae338eb9d: use z3-4.4.1 for arm64-linux, which often works like pre-4.4.0 and sometimes crashes.

Sat, Nov 27, 3:32 PM · provers
makarius added a comment to T31: Improve robustness of multithreaded Kodkod in Isabelle/Scala.

Back to external Java process for Isabelle2021-1 release (see 91ee232b4211).

Sat, Nov 27, 3:30 PM · isabelle-release
makarius closed T40: Potential problems with isabelle-dev mailing list server as Resolved.
Sat, Nov 27, 3:27 PM

Fri, Nov 26

Simon Wimmer <wimmers@in.tum.de> committed rAFPf8f7720a7451: fix dangerous context management.
fix dangerous context management
Fri, Nov 26, 10:39 PM
makarius committed rISABELLE5280c02f29dc: merged.
merged
Fri, Nov 26, 9:08 PM
makarius committed rISABELLEc5ce1e2f26ab: more robust build on midrange hardware (despite 67d6f1708ea4);.
more robust build on midrange hardware (despite 67d6f1708ea4);
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE2336356d4180: updated to polyml-5.9;.
updated to polyml-5.9;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLEa763f94c2c32: Added tag Isabelle2021-1-RC4 for changeset 2336356d4180.
Added tag Isabelle2021-1-RC4 for changeset 2336356d4180
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE743b114bdb41: NEWS on "isabelle mirabelle";.
NEWS on "isabelle mirabelle";
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE8fe987615ffe: tuned;.
tuned;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE90242c744a1a: maintain option kodkod_scala within theory context, to allow local modification;.
maintain option kodkod_scala within theory context, to allow local modification;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE91ee232b4211: clarified default for kodkod_scala;.
clarified default for kodkod_scala;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLEace8be1881e1: NEWS for proper release;.
NEWS for proper release;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE29672359a371: updated to flatlaf-1.6.4;.
updated to flatlaf-1.6.4;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE4faf0ec33cbf: option document_comment_latex supports e.g. Dagstuhl LIPIcs;.
option document_comment_latex supports e.g. Dagstuhl LIPIcs;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE3bf746911da1: more explicit type Latex.Tags;.
more explicit type Latex.Tags;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE9ad3fa47c83e: avoid broken links: auxiliary files are not yet supported;.
avoid broken links: auxiliary files are not yet supported;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLEf0e0fc82b0b9: removed pointless 'text_cartouche' command: regular 'text' already supports….
removed pointless 'text_cartouche' command: regular 'text' already supports…
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE4c8d9479f916: more uniform treatment of optional_argument for Latex elements;.
more uniform treatment of optional_argument for Latex elements;
Fri, Nov 26, 9:08 PM
makarius committed rISABELLEa97ec0954c50: example: alternative document headings, based on more general document output….
example: alternative document headings, based on more general document output…
Fri, Nov 26, 9:08 PM
makarius committed rISABELLE26c3a9c92e11: more general document output: enclosing markup is defined in user-space;.
more general document output: enclosing markup is defined in user-space;
Fri, Nov 26, 9:08 PM