- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Dec 27 2020
Dec 27 2020
updated for release;
proper NEWS according to current situation;
updated for release;
Disabled now (notably Isabelle2021-RC1), see Isabelle/6ead333e450d and AFP/2bccd7c8634c.
For improved portability (also for arm64-darwin) it might be better to exchange the app launcher as well, using a plain shell script instead of native executable.
tuned (see also b5333fc056da);
Dec 26 2020
Dec 26 2020
Dec 25 2020
Dec 25 2020
paulson <lp15@cam.ac.uk> committed rISABELLE83b114a6545f: A few more simprules for iff-reasoning.
A few more simprules for iff-reasoning
paulson <lp15@cam.ac.uk> committed rISABELLEcf14976d4fdb: infinite products iff simprule.
infinite products iff simprule
Dec 24 2020
Dec 24 2020
paulson <lp15@cam.ac.uk> committed rAFP222edcd0eb44: A little more tidying up.
A little more tidying up
paulson <lp15@cam.ac.uk> committed rAFP1e53550fa67e: more on "summable".
more on "summable"
paulson <lp15@cam.ac.uk> committed rISABELLE21c919addd8c: Two biconditional simprules for summable.
Two biconditional simprules for summable
support ISABELLE_APPLE_PLATFORM64 (Apple Silicon);
makarius committed rISABELLEa4efee8f8842: updated to sqlite-jdbc-3.34.0, with support for native arm64-darwin;.
updated to sqlite-jdbc-3.34.0, with support for native arm64-darwin;
makarius committed rISABELLE7ea253f93606: more robust: clarified error when merging Hoare_Logic + Hoare_Logic_Abort;.
more robust: clarified error when merging Hoare_Logic + Hoare_Logic_Abort;
makarius committed rISABELLEa562a0f656e8: more robust components_base: avoid fragile directory links on Windows (or….
more robust components_base: avoid fragile directory links on Windows (or…
Dec 23 2020
Dec 23 2020
clarified defaults: disabled in "isabelle build";
adapted to Isabelle/b1be35908165;
avoid memory problems on test machine;
makarius committed rISABELLE6ead333e450d: more robust defaults: spurious problems with parallel invocations and….
more robust defaults: spurious problems with parallel invocations and…
avoid multiple uses of the same ML file;
tuned document, notably authors and sections;
clarified presentation of files for each theory;
makarius committed rISABELLE52ba78df4088: disable auto_nitpick for now: spurious problems with non-termination e.g. in….
disable auto_nitpick for now: spurious problems with non-termination e.g. in…
makarius committed rISABELLEb1be35908165: clarified modules: avoid multiple uses of the same ML file;.
clarified modules: avoid multiple uses of the same ML file;
makarius committed rISABELLEd231d71d27b4: clarified session: avoid merge of different syntax from different Hoare logics;.
clarified session: avoid merge of different syntax from different Hoare logics;
makarius committed rISABELLE9cc431444435: clarified modules: avoid multiple uses of the same ML file;.
clarified modules: avoid multiple uses of the same ML file;
clarified syntax modes, avoid obsolete "xsymbols";
clarified fonts, notably for Windows L&F;
more friendly desktop application on macOS;
paulson <lp15@cam.ac.uk> committed rAFPc50a4d12d566: tidying for the new geometric simprule.
tidying for the new geometric simprule
paulson <lp15@cam.ac.uk> committed rISABELLE4fc3dc37f406: default simprule for geometric series.
default simprule for geometric series
paulson <lp15@cam.ac.uk> committed rAFP7db1c571f529: A bit of tidying up.
A bit of tidying up
Dec 22 2020
Dec 22 2020
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPd2b1144970c0: eliminate unnecessary assumption edge_antiparallel.
eliminate unnecessary assumption edge_antiparallel
Dec 21 2020
Dec 21 2020
less aggressive auto-build: avoid change of running jar;
clarified window size;
makarius committed rISABELLE51442c6dc296: more robust Java monitor: avoid odd warning about insecure connection;.
more robust Java monitor: avoid odd warning about insecure connection;
clarified modules;
clarified modules;
misc tuning for release;
makarius committed rISABELLE162b71f7e554: rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;.
rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
provide zipperposition-2.0 for experimentation;
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPf1b514b3a990: merged.
merged
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPf000868a784d: move theorems.
move theorems
desharna committed rISABELLE11de287ed481: tweaked tptp parsing when source info is missing.
tweaked tptp parsing when source info is missing
Dec 20 2020
Dec 20 2020
proper relative path;
present auxiliary files with PIDE markup;
tuned signature: more explicit types;
clarified signature and module structure;
makarius committed rISABELLE942bf91545fa: clarified comments: file-system access is always unsynchronized;.
clarified comments: file-system access is always unsynchronized;
more precise simpset for method unat_arith
more precise simpset for method unat_arith
Dec 19 2020
Dec 19 2020
clarified scope of concept
Lars Hupel <lars.hupel@mytum.de> committed rAFP32113098cca3: fix proof in Relational_Method.
fix proof in Relational_Method
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP414eeb34a872: update MFMC_Countable change log.
update MFMC_Countable change log
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPb2b67191f258: remove document generation again.
remove document generation again
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP6d89d20f7c88: Automated merge with https://foss.heptapod.net/isa-afp/afp-devel.
Automated merge with https://foss.heptapod.net/isa-afp/afp-devel
Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP93ca33f4d915: a simpler MFMC proof for bounded networks.
a simpler MFMC proof for bounded networks
clarified name
download auxiliary files via "curl";
clarified markup: open URL as editor file;
download as in Isabelle/Scala;
improved markup for theory header imports;
clarified markup (refining dd56ba1974e6);
more documentation;
Dec 18 2020
Dec 18 2020
makarius moved T30: Component and Isabelle/ML setup for Zipperposition from Backlog to TODO on the provers board.
makarius moved T31: Improve robustness of multithreaded Kodkod in Isabelle/Scala from Backlog to TODO on the isabelle-release board.
makarius moved T32: Odd font rendering problem with jdk-11.0.9 on Windows from Backlog to TODO on the isabelle-release board.
makarius moved T33: Update to jdk-11.0.10, notably for macOS Big Sur from Backlog to TODO on the isabelle-release board.
makarius moved T34: Update component for Vampire from Backlog to TODO on the isabelle-release board.
makarius moved T34: Update component for Vampire from TODO to Backlog 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 moved T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon) from TODO to Backlog on the isabelle-release board.
makarius moved T32: Odd font rendering problem with jdk-11.0.9 on Windows from TODO to Backlog on the isabelle-release board.
makarius moved T33: Update to jdk-11.0.10, notably for macOS Big Sur from TODO to Backlog on the isabelle-release board.
makarius moved T31: Improve robustness of multithreaded Kodkod in Isabelle/Scala from Backlog to TODO on the isabelle-release board.