User Details
User Details
- User Since
- Sep 24 2019, 9:33 PM (109 w, 9 h)
- Roles
- Administrator
Yesterday
Yesterday
tuned, continuing e955964d89cb;
makarius committed rISABELLE71bafd70acbb: avoid waste of resources due to dynamic simpset (amending 45c09620f726);.
avoid waste of resources due to dynamic simpset (amending 45c09620f726);
clarified modules;
more CONTRIBUTORS and NEWS;
more realistic timeout;
Mon, Oct 25
Mon, Oct 25
clarified signature, according to Isabelle/ccf599864beb;
more antiquotations;
more antiquotations;
makarius committed rISABELLEe5b38bb5a147: more robust: genuinely free variables need to be instantiated;.
more robust: genuinely free variables need to be instantiated;
makarius committed rISABELLEd4829a7333e2: clarified instantiation: local beta reduction after substitution, as for Envir..
clarified instantiation: local beta reduction after substitution, as for Envir.
clarified signature -- avoid clones;
Sun, Oct 24
Sun, Oct 24
makarius committed rISABELLEe2e2bc1f9570: avoid persistence of static context: instantiation arguments should provide….
avoid persistence of static context: instantiation arguments should provide…
more antiquotations;
clarified name, syntax, messages;
more antiquotations;
more control symbols;
ML antiquotations to instantiate types/terms/props;
Thu, Oct 21
Thu, Oct 21
tuned signature, according to Isabelle/042041c0ebeb;
Wed, Oct 20
Wed, Oct 20
discontinued obsolete "val extend = I" for data slots;
discontinued obsolete "val extend = I" for data slots;
clarified signature;
clarified keywords and reports;
clarified signature;
Tue, Oct 19
Tue, Oct 19
makarius renamed T10: Font rendering quality in OpenJDK 11 vs. 17 from Font rendering quality in OpenJDK 11 vs. 13 to Font rendering quality in OpenJDK 11 vs. 17.
makarius added a comment to T10: Font rendering quality in OpenJDK 11 vs. 17.
Isabelle2021-1 (December 2021) will use Java 17, but the font situation appears to be unchanged.
makarius added a comment to T29: Update component for Z3.
Not ready for the Isabelle2021-1 release, approx. 15-Dec-2021. Note that veriT is more and more taking over.
See Isabelle/d4c2a9191cd1
makarius added a comment to T31: Improve robustness of multithreaded Kodkod in Isabelle/Scala.
This requires to go through the Java implementation of Kodkod and SAT4j, and ensure that interrupts (or timeouts) are treated properly.
makarius closed T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon) as Resolved.
makarius added a comment to T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon).
See also Isabelle/74a36aae067a and Isabelle/2d089ff0e03b --- minisat is provided as external executable on all platforms.
makarius updated the post content for Blog Post: More robust (and more strict) treatment of abstractions within the context.
makarius updated the post content for Blog Post: More robust (and more strict) treatment of abstractions within the context.
tuned ML --- clarified use of context;
tuned --- fewer clones;
updated to jEdit plugin Highlight 2.5;
proper file headers;
proper tactic combinator;
more accurate treatment of context;
Mon, Oct 18
Mon, Oct 18
more accurate treatment of context;
adapted to Term.dest_abs_global / Logic.dest_all_global (e.g.
more accurate treatment of context;
tuned -- proper names/scopes for contexts;
more accurate treatment of context;
more accurate treatment of context;
makarius committed rAFP8f7185ecb827: proper antiquotations;.
proper antiquotations;
more accurate treatment of context;
makarius committed rAFP3b02b2ea9e9f: more maintainable Isabelle/ML: proper signatures, proper names/scopes for….
more maintainable Isabelle/ML: proper signatures, proper names/scopes for…
clarified signature, following Isabelle/de4f151c2a34;
more accurate treatment of context;
makarius committed rISABELLEf07761ee5a7f: more robust Variable.revert_bounds (see also b12f2cef3ee5);.
more robust Variable.revert_bounds (see also b12f2cef3ee5);
tuned -- proper names/scopes for contexts;
isabelle regenerate_cooper;
more accurate treatment of context;
revert bbfed17243af, breaks HOL-Proofs extraction;
proper p' instead of p (amending 52c7c42e7e27);
makarius committed rISABELLEc960bfcb91db: discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by….
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by…
proper context for Goal.prove_internal;
makarius committed rISABELLE8ee3d5d3c1bf: more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;.
more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
clarified signature;
Wed, Oct 13
Wed, Oct 13
clarified signature;
clarified signature;
clarified signature;