- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Jan 18 2021
Jan 18 2021
sterraf committed rAFP7f80012e5998: Adapted to 2021-RC2; renamed lemma ccc_Fn_nat -> ccc_Fn_2.
Adapted to 2021-RC2; renamed lemma ccc_Fn_nat -> ccc_Fn_2
Jan 17 2021
Jan 17 2021
sync Word_Lib with l4v
makarius committed rISABELLEca450d902198: updated to scala-2.13: its ArraySeq implementation is not usable here (requires….
updated to scala-2.13: its ArraySeq implementation is not usable here (requires…
updated to scala-2.13.4;
clarified return code: re-use SIGALRM for soft timeout;
makarius committed rISABELLEff6b5e468d5f: clarified signature: support more generic server implementations;.
clarified signature: support more generic server implementations;
clarified signature: more operations;
adapted to scala-2.13.4;
Jan 16 2021
Jan 16 2021
paulson <lp15@cam.ac.uk> committed rAFPc7606b58bd03: removed a terrible default simprule.
removed a terrible default simprule
Jan 15 2021
Jan 15 2021
Jan 14 2021
Jan 14 2021
paulson <lp15@cam.ac.uk> committed rISABELLE4c4d479b097d: new magerial from Jakub Kądziołka.
new magerial from Jakub Kądziołka
Jan 13 2021
Jan 13 2021
CSP_RefTK: adjust for Isabelle 1105c42722dc
sitegen for CSP_RefTK
New submission: CSP_RefTK
paulson <lp15@cam.ac.uk> committed rAFP89ed1831f6cd: New (ZF!) entry Delta_System_Lemma.
New (ZF!) entry Delta_System_Lemma
paulson <lp15@cam.ac.uk> committed rAFP2da14e4d854f: webpage for Delta_System_Lemma.
webpage for Delta_System_Lemma
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa80f4e41ac2b: sitegen and metadata.
sitegen and metadata
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP85bc7487435c: new entry: Topological_Semantics.
new entry: Topological_Semantics
Jan 12 2021
Jan 12 2021
tuned image size: scale 0.2;
updated screenshot;
Jan 10 2021
Jan 10 2021
makarius lowered the priority of T35: Isabelle/jEdit full-screen problem with macOS Big Sur from High to Normal.
Works better with work-around, as documented in Isabelle/6345ad861a36.
back to post-release mode;
Added tag Isabelle2021-RC2 for changeset 802647edfe7b
avoid Unicode quotes;
clarified pretty margin: attempt to avoid scrollbar;
more documentation;
makarius committed rISABELLEc3589f2dff31: more informative errors: simplify diagnosis of spurious failures reported by….
more informative errors: simplify diagnosis of spurious failures reported by…
makarius added a comment to rISABELLE9480a9efe19e: proper size of buttons in Symbols dockable, e.g. \<A> 0x01d49c vs. \<B>….
See also https://github.com/JFormDesigner/FlatLaf/issues/234 (already closed).
Jan 9 2021
Jan 9 2021
makarius committed rISABELLE83a2b6976515: proper labels for status message: "sidekick.parsing-complete={0} parsing….
proper labels for status message: "sidekick.parsing-complete={0} parsing…
clarified list of presented look-and-feels;
makarius committed rISABELLE9480a9efe19e: proper size of buttons in Symbols dockable, e.g. \<A> 0x01d49c vs. \<B>….
proper size of buttons in Symbols dockable, e.g. \<A> 0x01d49c vs. \<B>…
makarius committed rISABELLEb84887a67cc6: clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);.
clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);
makarius committed rISABELLEa8e5d7c9a834: discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it….
discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it…
pruvisto committed rISABELLE9bf36baa8686: Corrected lemma that was too specific in HOL-Computational_Algebra.
Corrected lemma that was too specific in HOL-Computational_Algebra
Avoid problem by using FlatLaf: Isabelle/efc58b56a6c7.
Avoid problem by using FlatLaf: Isabelle/efc58b56a6c7.
tuned GUI, notably for scalable FlatLaf;
updated to Isabelle/efc58b56a6c7;
clarified default L&F;
support for additional look-and-feels;
Jan 8 2021
Jan 8 2021
makarius committed rISABELLEc87ca43ebd3b: avoid rescaled fonts, e.g. dockable buttons on Windows L&F after opening a new….
avoid rescaled fonts, e.g. dockable buttons on Windows L&F after opening a new…
Algebraic_Numbers: some material on algebraic integers
pruvisto committed rISABELLE783406dd051e: some algebra material for HOL: characteristic of a ring, algebraic integers.
some algebra material for HOL: characteristic of a ring, algebraic integers
pruvisto committed rISABELLE981a383610df: HOL-Data_Structures: added Selection and time functions for list functions.
HOL-Data_Structures: added Selection and time functions for list functions
makarius committed rISABELLE3df45de0c079: discontinued body_range (again): does not quite work, because Position..
discontinued body_range (again): does not quite work, because Position.
makarius committed rISABELLE578a33042aa6: clarified: command keyword position is sufficient (amending 693a39f2cddc);.
clarified: command keyword position is sufficient (amending 693a39f2cddc);
tuned -- avoid old-style verbatim text;
isabelle update_cartouches;
mathias.fleury committed rISABELLE6520d59fbdd7: ignore error messages produced by CVC4 when generating BV.
ignore error messages produced by CVC4 when generating BV
paulson <lp15@cam.ac.uk> committed rAFP7e9db34de4f6: A bit of tidying.
A bit of tidying
paulson <lp15@cam.ac.uk> committed rISABELLEb69fd6e19662: One useful lemma/simprule.
One useful lemma/simprule
isabelle update_cartouches;
tuned --- prefer explicit position;
makarius committed rISABELLE693a39f2cddc: recovered body_range from eca176f773e0 --- its Command.core_range is in….
recovered body_range from eca176f773e0 --- its Command.core_range is in…
makarius committed rISABELLE8a20737e4ebf: support more command positions, analogous to Command.core_range in….
support more command positions, analogous to Command.core_range in…
more uniform core_range (amending def3ec9cdb7e);
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP29cb2568407d: reform.
reform
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP55b144f95853: added code-post lemma for algebraic numbers.
added code-post lemma for algebraic numbers
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP306f9dbda4f6: proper indentation.
proper indentation
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP7661a1e15035: moved lemmas such that algebraic numbers theory is not importing factorization….
moved lemmas such that algebraic numbers theory is not importing factorization…
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP95ca3e871eb7: moved lemmas.
moved lemmas
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1a49a0b2203e: cleanup.
cleanup
Julian Brunner <julianbrunner@gmail.com> committed rAFPc1ae04538bfe: merged.
merged
Julian Brunner <julianbrunner@gmail.com> committed rAFPd3642bed65b1: fix long-running proof.
fix long-running proof
Julian Brunner <julianbrunner@gmail.com> committed rAFP5d1dd3139576: updated benchmark scripts for iFM paper.
updated benchmark scripts for iFM paper
Peter Gammie <peteg42@gmail.com> committed rAFPf972abc8ec2e: Update ConcurrentGC.
Update ConcurrentGC
Peter Gammie <peteg42@gmail.com> committed rAFP5ee9691b6e09: Update ConcurrentIMP.
Update ConcurrentIMP
Jan 7 2021
Jan 7 2021
- use jdk-15 in Isabelle/af54129abd9e
- OK: arm64-darwin and portable app launcher, e.g. see Isabelle/d08cbc36a99a
- OK: file associations work properly
- OPEN: full-screen mode, see T35: Isabelle/jEdit full-screen problem with macOS Big Sur
- OPEN: JTabbedPane, see T36: Bad rendering of JTabbedPane on macOS BigSur
clarified dock icon: setup earlier on startup;
makarius moved T34: Update component for Vampire from TODO to Backlog on the isabelle-release board.
It is unclear how to address this properly, without an update by Apple or OpenJDK (not to be expected too soon).
makarius moved T35: Isabelle/jEdit full-screen problem with macOS Big Sur from Backlog to TODO on the isabelle-release board.
makarius moved T31: Improve robustness of multithreaded Kodkod in Isabelle/Scala from TODO to Backlog on the isabelle-release board.
makarius renamed T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon) from Missing minisat.dll for nitpick/kodkod on Windows to Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon).