diff --git a/.hgignore b/.hgignore
--- a/.hgignore
+++ b/.hgignore
@@ -1,23 +1,22 @@
syntax: glob
*~
*.class
*.jar
*.marks
*.orig
*.rej
.DS_Store
.swp
syntax: regexp
^contrib
^heaps/
^browser_info/
^doc/.*\.pdf
^lib/classes/
-^src/Tools/jEdit/dist/
^src/Tools/VSCode/out/
^src/Tools/VSCode/extension/node_modules/
^Admin/jenkins/ci-extras/target/
diff --git a/Admin/Release/CHECKLIST b/Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST
+++ b/Admin/Release/CHECKLIST
@@ -1,99 +1,101 @@
Checklist for official releases
===============================
- check latest updates of polyml, jdk, scala, jedit;
- check Admin/components;
- test "isabelle dump -b Pure ZF";
- test "isabelle build -o export_theory -f ZF";
- test "isabelle server" according to "system" manual;
- test Isabelle/VSCode;
- test Isabelle/jEdit: print buffer
+- test Isabelle/jEdit: deactivate main plugin;
+
- test "#!/usr/bin/env isabelle_scala_script";
- test Windows 10 subsystem for Linux:
https://docs.microsoft.com/en-us/windows/wsl/install-win10
- check (non-)executable files:
$ find . "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" -o -name ROOT ")" -executable
$ find -type f -executable
- check sources:
isabelle check_sources '~~' '$AFP_BASE'
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
- check versions:
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src-base/Isabelle_Base.props
- check Isabelle version:
src/Tools/VSCode/extension/README.md
src/Tools/VSCode/extension/package.json
- check funny base directory, e.g. "Test 中国";
- diff NEWS wrt. last official release, which is read-only;
- update https://isabelle.sketis.net/repos/isabelle-website
-- check doc/Contents, src/Tools/jEdit/dist/doc/Contents;
+- check doc/Contents, $JEDIT_HOME/doc/Contents;
- test old HD display: Linux, Windows, macOS;
- macOS: check recent MacTeX;
- Windows: check recent MiKTeX;
- Phabricator:
. src/Doc/System/Phabricator.thy: check/update underlying Ubuntu version
. etc/options: check/update phabricator_version entries;
Repository fork
===============
- isabelle: finalize NEWS / CONTRIBUTORS -- proper headers for named release;
- isabelle-release: hg tag;
- isabelle: back to post-release mode -- after fork point;
Packaging
=========
- macOS: provide "gnutar" executable via shell PATH
(e.g. copy of /usr/bin/gnutar from Mountain Lion)
- fully-automated packaging (e.g. on lxcisa0):
hg up -r DISTNAME && Admin/build_release -D /home/isabelle/dist -b HOL -l -R DISTNAME
- Docker image:
isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz
docker login
docker push makarius/isabelle:Isabelle2021
docker tag ... latest
docker push makarius/isabelle:latest
https://hub.docker.com/r/makarius/isabelle
https://docs.docker.com/engine/reference/commandline/push
Post-release
============
- update Admin/Release/official
- update /home/isabelle and /home/isabelle/html-data
diff --git a/Admin/Windows/launch4j/isabelle.xml b/Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml
+++ b/Admin/Windows/launch4j/isabelle.xml
@@ -1,41 +1,41 @@
true
gui
{OUTFILE}
normal
false
false
{ICON}
- isabelle.Main
+ isabelle.jedit.Main
{CLASSPATH}
{ISABELLE_NAME}
{ISABELLE_NAME}
%EXEDIR%\contrib\jdk\x86_64-windows
true
false
jdkOnly
64
-splash:"%EXEDIR%\lib\logo\isabelle.gif" -Disabelle.root="%EXEDIR%" -Dcygwin.root="%EXEDIR%\contrib\cygwin"
{SPLASH}
true
120
false
\ No newline at end of file
diff --git a/Admin/build b/Admin/build
--- a/Admin/build
+++ b/Admin/build
@@ -1,91 +1,88 @@
#!/usr/bin/env bash
#
# Administrative build for Isabelle source distribution.
## directory layout
if [ -z "$ISABELLE_HOME" ]; then
unset CDPATH
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
fi
## diagnostics
PRG="$(basename "$0")"
function usage()
{
cat <&2
exit 2
}
## process command line
[ "$#" -eq 0 ] && usage
MODULES="$@"; shift "$#"
## modules
function build_all ()
{
build_browser
- build_jars
+ build_setup build
}
function build_browser ()
{
pushd "$ISABELLE_HOME/lib/browser" >/dev/null
"$ISABELLE_TOOL" env ./build || exit $?
popd >/dev/null
}
-function build_jars ()
+function build_setup ()
{
- pushd "$ISABELLE_HOME" >/dev/null
- "$ISABELLE_TOOL" env src/Pure/build-jars "$@" || exit $?
- popd >/dev/null
+ rm -rf \
+ "$ISABELLE_HOME/lib/classes/Pure.jar" \
+ "$ISABELLE_HOME/lib/classes/Pure.shasum" \
+ "$ISABELLE_HOME/src/Tools/jEdit/dist"
+ env ISABELLE_SETUP_CLASSPATH_SKIP=true "$ISABELLE_TOOL" java isabelle.setup.Setup "$@"
}
## main
-#FIXME workarounds for scalac 2.11.0
-export CYGWIN="nodosfilewarning"
-function stty() { :; }
-export -f stty
-
for MODULE in $MODULES
do
case $MODULE in
all) build_all;;
browser) build_browser;;
- jars) build_jars;;
- jars_fresh) build_jars -f;;
+ jars) build_setup build;;
+ jars_fresh) build_setup build_fresh;;
*) fail "Bad module $MODULE"
esac
done
diff --git a/Admin/components/components.sha1 b/Admin/components/components.sha1
--- a/Admin/components/components.sha1
+++ b/Admin/components/components.sha1
@@ -1,419 +1,421 @@
59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz
ed740867925dcf58692c8d3e350c28e3b4d4a60f Isabelle_app-20210126.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz
8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz
fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz
bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz
81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz
97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz
5c5b7c18cc1dc2a4d22b997dac196da09eaca868 bash_process-1.2.3-1.tar.gz
48b01bd9436e243ffcb7297f08b498d0c0875ed9 bash_process-1.2.3.tar.gz
11815d5f3af0de9022e903ed8702c136591f06fe bash_process-1.2.4-1.tar.gz
729486311833e4eff0fbf2d8041dddad520ca88c bash_process-1.2.4-2.tar.gz
7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee bash_process-1.2.4.tar.gz
9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz
a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz
4085dd6060a32d7e0d2e3f874c463a9964fd409b bib2xhtml-20190409.tar.gz
f92cff635dfba5d4d77f469307369226c868542c cakeml-2.0.tar.gz
e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz
e880f31f59bd403fb72fcd3b5afb413c3831a21c csdp-6.1-1.tar.gz
2659100ba8e28e7cb0ecb554178ee5315d4a87f5 csdp-6.1.1.tar.gz
a2bd94f4f9281dc70dfda66cf28016c2ffef7ed7 csdp-6.1.tar.gz
ec17080269737e4a97b4424a379924c09b338ca2 csdp-6.2.0.tar.gz
70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
d70bfbe63590153c07709dea7084fbc39c669841 cvc4-1.5-1.tar.gz
541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz
1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz
c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz
ffb0d4739c10eb098eb092baef13eccf94a79bad cvc4-1.5-5.tar.gz
3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz
a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz
4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz
b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz
76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz
03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz
e99560d0b7cb9bafde2b0ec1a3a95af315918a25 cvc4-1.8.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
1fde9ddf0fa4f398965113d0c0c4f0e97c78d008 cygwin-20130716.tar.gz
a03735a53c2963eb0b453f6a7282d3419f28bf38 cygwin-20130916.tar.gz
7470125fc46e24ee188bdaacc6d560e01b6fa839 cygwin-20140520.tar.gz
db4dedae026981c5f001be283180abc1962b79ad cygwin-20140521.tar.gz
acbc4bf161ad21e96ecfe506266ccdbd288f8a6f cygwin-20140530.tar.gz
3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41 cygwin-20140626.tar.gz
8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz
238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz
629b8fbe35952d1551cd2a7ff08db697f6dff870 cygwin-20141024.tar.gz
ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c cygwin-20150410.tar.gz
fa712dd5ec66ad16add1779d68aa171ff5694064 cygwin-20151210.tar.gz
056b843d5a3b69ecf8a52c06f2ce6e696dd275f9 cygwin-20151221.tar.gz
44f3a530f727e43a9413226c2423c9ca3e4c0cf5 cygwin-20161002.tar.gz
dd56dd16d861fc6e1a008bf5e9da6f33ed6eb820 cygwin-20161022.tar.gz
d9ad7aae99d54e3b9813151712eb88a441613f04 cygwin-20161024.tar.gz
f8eb6a0f722e3cfe3775d1204c5c7063ee1f008e cygwin-20170828.tar.gz
c22048912b010a5a0b4f2a3eb4d318d6953761e4 cygwin-20170930.tar.gz
5a3919e665947b820fd7f57787280c7512be3782 cygwin-20180604.tar.gz
2aa049170e8088de59bd70eed8220f552093932d cygwin-20190320.tar.gz
fb898e263fcf6f847d97f564fe49ea0760bb453f cygwin-20190322.tar.gz
cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1 cygwin-20190524.tar.gz
caa616fbab14c1fce790a87db5c4758c1322cf28 cygwin-20200116.tar.gz
f053a9ab01f0be9cb456560f7eff66a8e7ba2fd2 cygwin-20200323.tar.gz
0107343cd2562618629f73b2581168f0045c3234 cygwin-20201002.tar.gz
a3d481401b633c0ee6abf1da07d75da94076574c cygwin-20201130.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz
c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz
a895a96ec7e6fcc275114bb9b4c92b20fac73dba e-2.0-1.tar.gz
2ebd7e3067a2cdae3cb8b073345827013978d74b e-2.0-2.tar.gz
fac44556dd16f666a2c186be30aa6d8c67228bb9 e-2.0-3.tar.gz
5d36fb62912cfcff7f3b99a6266c578aafc288b7 e-2.0-4.tar.gz
3223c51c0b16fe00ced4ae903041fff858e61742 e-2.0-5.tar.gz
6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz
66449a7b68b7d85a7189e10735a81069356123b6 e-2.5-1.tar.gz
813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz
6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz
ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz
d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz
dac46ce81cee10fb36a9d39b414dec7b7b671545 flatlaf-1.0-rc2.tar.gz
d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz
7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz
9908e5ab721f1c0035c0ab04dc7ad0bd00a8db27 flatlaf-1.2.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz
20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz
9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz
f5c63689a394b974ac0d365debda577c6fa31c07 isabelle_fonts-20151107.tar.gz
812101680b75f7fa9ee8e138ea6314fa4824ea2d isabelle_fonts-20151229.tar.gz
2730e1475c7d655655882e75743e0b451725a274 isabelle_fonts-20151231.tar.gz
1f004a6bf20088a7e8f1b3d4153aa85de6fc1091 isabelle_fonts-20160101.tar.gz
379d51ef3b71452dac34ba905def3daa8b590f2e isabelle_fonts-20160102.tar.gz
878536aab1eaf1a52da560c20bb41ab942971fa3 isabelle_fonts-20160227.tar.gz
8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz
9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz
620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz
b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz
c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz
3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz
bee32019e5d7cf096ef2ea1d836c732e9a7628cc isabelle_fonts-20181124.tar.gz
f249bc2c85bd2af9eee509de17187a766b74ab86 isabelle_fonts-20181129.tar.gz
928b5320073d04d93bcc5bc4347b6d01632b9d45 isabelle_fonts-20190210.tar.gz
dfcdf9a757b9dc36cee87f82533b43c58ba84abe isabelle_fonts-20190309.tar.gz
95e3acf038df7fdeeacd8b4769930e6f57bf3692 isabelle_fonts-20190406.tar.gz
dabcf5085d67c99159007007ff0e9bf775e423d1 isabelle_fonts-20190409.tar.gz
76827987c70051719e117138858930d42041f57d isabelle_fonts-20190717.tar.gz
abc8aea3ae471f9313917008ac90e5c1c99e17da isabelle_fonts-20210317.tar.gz
3ff9195aab574fc75ca3b77af0adb33f9b6d7b74 isabelle_fonts-20210318.tar.gz
b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
e413706694b0968245ee15183af2d464814ce0a4 isabelle_setup-20210711.tar.gz
+d2c9fd7b73457a460111edd6eb93a133272935fb isabelle_setup-20210715.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
06ac8993b5bebd02c70f1bd18ce13075f01115f3 jdk-11.0.3+7.tar.gz
e7e3cc9b0550c1e5d71197ad8c30f92b622d7183 jdk-11.0.4+11.tar.gz
49007a84a2643a204ce4406770dfd574b97880d9 jdk-11.0.5+10.tar.gz
3c250e98eb82f98afc6744ddc9170d293f0677e1 jdk-11.0.6+10.tar.gz
76cf7a141e15db30bd975089c65c833b58092aa7 jdk-11.0.9+11.tar.gz
71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz
72455a2fdb6cced9cd563f4d5d6134f7a6c34913 jdk-15.0.1+9.tar.gz
e8ae300e61b0b121018456d50010b555bc96ce10 jdk-15.0.2+7.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz
5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz
dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz
ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz
e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz
d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz
b66039bc6dc2bdb2992133743005e1e4fc58ae24 jdk-7u72.tar.gz
d980055694ddfae430ee001c7ee877d535e97252 jdk-7u76.tar.gz
baa6de37bb6f7a104ce5fe6506bca3d2572d601a jdk-7u80.tar.gz
7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
baf275a68d3f799a841932e4e9a95a1a604058ae jdk-8u102.tar.gz
5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
741de6a4a805a0f9fb917d1845409e99346c2747 jdk-8u112.tar.gz
ae7df8bd0c18eb40237cf54cc28933f4893b9c92 jdk-8u121.tar.gz
51531a3a0c16e180ed95cb7d2bd680c2ec0aa553 jdk-8u131.tar.gz
e45edcf184f608d6f4a7b966d65a5d3289462693 jdk-8u144.tar.gz
264e806b9300a4fb3b6e15ba0e2c664d4ea698c8 jdk-8u152.tar.gz
84b04d877a2ea3a4e2082297b540e14f76722bc5 jdk-8u162.tar.gz
87303a0de3fd595aa3857c8f7cececa036d6ed18 jdk-8u172.tar.gz
9ae0338a5277d8749b4b4c7e65fc627319d98b27 jdk-8u181.tar.gz
cfecb1383faaf027ffbabfcd77a0b6a6521e0969 jdk-8u20.tar.gz
44ffeeae219782d40ce6822b580e608e72fd4c76 jdk-8u31.tar.gz
c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz
4132cf52d5025bf330d53b96a5c6466fef432377 jdk-8u51.tar.gz
74df343671deba03be7caa49de217d78b693f817 jdk-8u60.tar.gz
dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz
2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz
caa0cf65481b6207f66437576643f41dabae3c83 jdk-8u92.tar.gz
+778fd85c827ec49d2d658a832d20e63916186b0d jedit-20210715.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
9c221fe71af8a063fcffcce21672a97aea0a8d5b jedit_build-20120313.tar.gz
ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz
6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz
7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz
8e1d36f5071e3def2cb281f7fefe9f52352cb88f jedit_build-20120903.tar.gz
8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz
06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz
c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz
5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz
054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz
4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz
a9d637a30f6a87a3583f265da51e63e3619cff52 jedit_build-20140722.tar.gz
f29391c53d85715f8454e1aaa304fbccc352928f jedit_build-20141018.tar.gz
d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4 jedit_build-20141026.tar.gz
f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz
14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.tar.gz
b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz
8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz
c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz
d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz
d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz
7bcb202e13358dd750e964b2f747664428b5d8b3 jedit_build-20180417.tar.gz
23c8a05687d05a6937f7d600ac3aa19e3ce59c9c jedit_build-20180504.tar.gz
9c64ee0705e5284b507ca527196081979d689519 jedit_build-20181025.tar.gz
cfa65bf8720b9b798ffa0986bafbc8437f44f758 jedit_build-20181026.tar.gz
847492b75b38468268f9ea424d27d53f2d95cef4 jedit_build-20181203.tar.gz
536a38ed527115b4bf2545a2137ec57b6ffad718 jedit_build-20190120.tar.gz
58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz
ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz
1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz
533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz
0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz
a0744f1948abdde4bfb51dd4769b619e7444baf1 jedit_build-20210510-1.tar.gz
837d6c8f72ecb21ad59a2544c69aadc9f05684c6 jedit_build-20210510.tar.gz
7bdae3d24b10261f6cb277446cf9ecab6062bd6f jedit_build-20210708.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
d84b7d8ef273afec55284327fca7dd20f5ecb77a jfreechart-1.5.1.tar.gz
c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
2155e0bdbd29cd3d2905454de2e7203b9661d239 jortho-1.0-2.tar.gz
ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
afb04f4048a87bb888fe7b05b0139cb060c7925b kodkodi-1.5.2-1.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
0634a946b216f7f07f1a0f7e28cf345daa28828f kodkodi-1.5.3.tar.gz
52e95b3493d71902f9df89d0bb59d0046a5f0c63 kodkodi-1.5.4-1.tar.gz
267189c637de26cf304d699cfa95389da002b250 kodkodi-1.5.4.tar.gz
3ecdade953bb455ed2907952be287d7e5cf6533b kodkodi-1.5.5.tar.gz
8aa939f5127290eb9a99952d375be9ffbf90c43b kodkodi-1.5.6-1.tar.gz
6b12bf3f40b16fae8ff22aa39171fa018d107cb3 kodkodi-1.5.6.tar.gz
377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz
1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz
3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz
0fbc826e4fcb95bb9e1814642f7fce788e7fe1c3 naproche-20210122-1.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz
810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
9c02ecf93863c3289002c5e5ac45a83e2505984c naproche-755224402e36.tar.gz
e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz
26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz
fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz
eb499a18e7040ca0fe1ca824c9dcb2087c47c9ba opam-2.0.3-1.tar.gz
002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz
ddb3b438430d9565adbf5e3d913bd52af8337511 opam-2.0.6.tar.gz
fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz
1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz
36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz
36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz
a588640dbf5da9ae15455b02ef709764a48637dc polyml-5.5.2-1.tar.gz
4b690390946f7bfb777b89eb16d6f08987cca12f polyml-5.5.2-2.tar.gz
5b31ad8556e41dfd6d5e85f407818be399aa3d2a polyml-5.5.2-3.tar.gz
532f6e8814752aeb406c62fabcfd2cc05f8a7ca8 polyml-5.5.2.tar.gz
1c53f699d35c0db6c7cf4ea51f2310adbd1d0dc5 polyml-5.5.3-20150820.tar.gz
b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a polyml-5.5.3-20150908.tar.gz
b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz
1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz
f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz
21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz
03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz
822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz
bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz
5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz
5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz
80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz
381a70cecf0fdee47f6842e2bdb5107ed52adab6 polyml-5.7.1-1.tar.gz
39dac33b569ac66f76126b8f4edc6d9227bd8a63 polyml-5.7.1-2.tar.gz
0b896ccc35bd3f2541cd55e6f0ed14637ed9fc68 polyml-5.7.1-4.tar.gz
262450ac9966abebae2e1d4f9ae703cfe0f5d8d9 polyml-5.7.1-5.tar.gz
1aeb57877d694db7fe4d4395287cddf3bc77710b polyml-5.7.1-6.tar.gz
e3e7e20b1e0e5d5d68df4cd4caa1e1a7410d46b6 polyml-5.7.1-7.tar.gz
1430533c09b17f8be73798a47a5f409d43a04cf4 polyml-5.7.1-8.tar.gz
171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz
5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz
51e024225b460900da5279f0b91b217085f98cf9 polyml-5.8-20190220.tar.gz
20a83fa58d497b533150defe39bcd4540529b25f polyml-5.8-20190306.tar.gz
9f0e9cd10df4c3383b063eb076e8b698ca50c3d0 polyml-5.8.1-20191101.tar.gz
f46deb909d645ac8c140968e4d32b5763beb9add polyml-5.8.1-20191113.tar.gz
36a40a981b57daae0463d14940a8edf6fa1af179 polyml-5.8.1-20191114.tar.gz
525b05536b08c11a1eae943fe6818a8622326084 polyml-5.8.1-20191124.tar.gz
9043828803483ca14df64488dff014ad050a6d34 polyml-5.8.1-20200228.tar.gz
1186607e2c43b77db86731f12fbedb531ca50a21 polyml-5.8.1-20200708.tar.gz
22ae16bf7850e73b903d2ca8eb506da05b441cf3 polyml-5.8.1.tar.gz
cb8e85387315f62dcfc6b21ec378186e58068f76 polyml-5.8.2.tar.gz
d1fd6eced69dc1df7226432fcb824568e0994ff2 polyml-5.8.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz
a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz
4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
85bfda83d138e936fdafd68ed3627b1058e5c2c3 polyml-test-7e49fce62e3d.tar.gz
c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz
7df4857d73dbc9edda25a6ad329e47639e70fadf polyml-test-8fda4fd22441.tar.gz
2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz
3dfdc58e5d9b28f038a725e05c9c2f2ce0bb2632 polyml-test-a3cfdf648da-1.tar.gz
e2f075b0cc709f4f7f6492b725362f9010b2c6d1 polyml-test-a3cfdf648da-2.tar.gz
33568f69ce813b7405386ddbefa14ad0342bb8f0 polyml-test-a3cfdf648da.tar.gz
4bedaac4f1fb9a9199aa63695735063c47059003 polyml-test-a444f281ccec.tar.gz
f3031692edcc5d8028a42861e4e40779f0f9d3e1 polyml-test-b68438d33c69.tar.gz
cb2318cff6ea9293cd16a4435a4fe28ad9dbe0b8 polyml-test-cf46747fee61.tar.gz
67ffed2f98864721bdb1e87f0ef250e4c69e6160 polyml-test-d68c6736402e.tar.gz
b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz
609c7d09d3ed01156ff91261e801e2403ff93729 polyml-test-e8d82343b692.tar.gz
b6d87466e9b44e8ef4a2fac74c96b139080a506a polyml-test-f54aa41240d0.tar.gz
d365f3fc11c2427cafc62b3c79951880a1476ebb polyml-test-f86ae3dc1686.tar.gz
a619177143fea42a464f49bb864665407c07a16c polyml-test-fb4f42af00fa.tar.gz
53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz
3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz
7d6ef4320d5163ceb052eb83c1cb3968f099a422 postgresql-42.2.18.tar.gz
e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40 postgresql-42.2.2.tar.gz
231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz
6335fbc0658e447b5b9bc48c9ad36e33a05bb72b postgresql-42.2.9.tar.gz
f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz
0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz
207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz
21c8ee274ffa471ab54d4196ecd827bf3d43e591 scala-2.10.3.tar.gz
d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz
44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz
14f20de82b25215a5e055631fb147356400625e6 scala-2.11.1.tar.gz
4fe9590d08e55760b86755d3fab750e90ac6c380 scala-2.11.2.tar.gz
27a296495b2167148de06314ed9a942f2dbe23fe scala-2.11.4.tar.gz
4b24326541161ce65424293ca9da3e7c2c6ab452 scala-2.11.5.tar.gz
e7cf20e3b27c894c6127c7a37042c1667f57385e scala-2.11.6.tar.gz
4810c1b00719115df235be1c5991aa6ea7186134 scala-2.11.7.tar.gz
3eca4b80710996fff87ed1340dcea2c5f6ebf4f7 scala-2.11.8.tar.gz
0004e53f885fb165b50c95686dec40d99ab0bdbd scala-2.12.0.tar.gz
059cbdc58d36e3ac1fffcccd9139ecd34f271882 scala-2.12.10.tar.gz
82056106aa6fd37c159ea76d16096c20a749cccd scala-2.12.11.tar.gz
fe7ff585acffaad7f0dd4a1d079134d15c26ed0d scala-2.12.12.tar.gz
74a8c3dab3a25a87357996ab3e95d825dc820fd0 scala-2.12.2.tar.gz
d66796a68ec3254b46b17b1f8ee5bcc56a93aacf scala-2.12.3.tar.gz
1636556167dff2c191baf502c23f12e09181ef78 scala-2.12.4.tar.gz
8171f494bba54fb0d01c887f889ab8fde7171c2a scala-2.12.5.tar.gz
54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz
02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz
201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz
edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.tar.gz
43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz
b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz
e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz
27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz
4d17611857fa3a93944c1f159c0fd2a161967aaf sqlite-jdbc-3.27.2.1.tar.gz
806be457eb79408fcc5a72aeca3f64b2d89a6b63 sqlite-jdbc-3.30.1.tar.gz
cba2b194114216b226d75d49a70d1bd12b141ac8 sqlite-jdbc-3.32.3.2.tar.gz
29306acd6ce9f4c87032b2c271c6df035fe7d4d3 sqlite-jdbc-3.34.0.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz
fdc415284e031ee3eb2f65828cbc6945736fe995 stack-1.9.1.tar.gz
6e19948ff4a821e2052fc9b3ddd9ae343f4fcdbb stack-1.9.3.tar.gz
f969443705aa8619e93af5b34ea98d15cd7efaf1 stack-2.1.3.tar.gz
ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.tar.gz
1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz
601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz
14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz
44d67b6742919ce59a42368fc60e2afa210a3e42 sumatra_pdf-2.5.2.tar.gz
89719a13bc92810730a430973684629426ed1b2a sumatra_pdf-3.0.tar.gz
f5afcc82f8e734665d38867e99475d3ad0d5ed15 sumatra_pdf-3.1.1.tar.gz
a45eca5c1277f42f87bb8dc12a3074ccf5488221 sumatra_pdf-3.1.2-1.tar.gz
3b3239b2e6f8062b90d819f3703e30a50f4fa1e7 sumatra_pdf-3.1.2-2.tar.gz
8486387f61557147ec06b1f637117c017c8f0528 sumatra_pdf-3.1.2.tar.gz
869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz
399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz
98c5c79fef7256db9f64c8feea2edef0a789ce46 verit-2016post.tar.gz
52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d verit-2020.10-rmx-1.tar.gz
b6706e74e20e14038e9b38f0acdb5639a134246a verit-2020.10-rmx.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz
e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz
8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz
d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz
c368908584e2bca38b3bcb20431d0c69399fc2f0 windows_app-20131130.tar.gz
c3f5285481a95fde3c1961595b4dd0311ee7ac1f windows_app-20131201.tar.gz
14807afcf69e50d49663d5b48f4b103f30ae842b windows_app-20150821.tar.gz
ed106181510e825bf959025d8e0a2fc3f78e7a3f windows_app-20180417.tar.gz
e809e4ab0d33cb413a7c47dd947e7dbdfcca1c24 windows_app-20181002.tar.gz
9e96ba128a0617a9020a178781df49d48c997e19 windows_app-20181006.tar.gz
1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz
2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz
c22196148fcace5443a933238216cff5112948df xz-java-1.5.tar.gz
4368ee09154dff42666a8c87e072261745619e51 xz-java-1.6.tar.gz
63f5fa09e92a895cb9aea27d7142abc86c487d25 xz-java-1.8.tar.gz
4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz
3a8f77822278fe9250890e357248bc678d8fac95 z3-3.2-1.tar.gz
12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz
d94a716502c8503d63952bcb4d4176fac8b28704 z3-4.0.tar.gz
86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz
a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz
06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz
93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz
b1bc411c2083fc01577070b56b94514676f53854 z3-4.4.0pre-2.tar.gz
4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz
517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz
b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
diff --git a/Admin/components/main b/Admin/components/main
--- a/Admin/components/main
+++ b/Admin/components/main
@@ -1,31 +1,31 @@
#main components for repository clones or release bundles
gnu-utils-20210414
bash_process-1.2.4-2
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
e-2.5-1
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
-isabelle_setup-20210711
+isabelle_setup-20210715
jdk-15.0.2+7
-jedit_build-20210708
+jedit-20210715
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
nunchaku-0.5
opam-2.0.7
polyml-5.8.2
postgresql-42.2.18
scala-2.13.5
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.34.0
ssh-java-20190323
stack-2.5.1
vampire-4.2.2
verit-2020.10-rmx-1
xz-java-1.8
z3-4.4.0pre-3
zipperposition-2.0-1
diff --git a/Admin/etc/build.props b/Admin/etc/build.props
new file mode 100644
--- /dev/null
+++ b/Admin/etc/build.props
@@ -0,0 +1,4 @@
+description = Isabelle/Scala/Admin
+lib = $ISABELLE_HOME/lib/classes
+name = isabelle_admin
+services = isabelle.Admin_Tools
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,16484 +1,16487 @@
Isabelle NEWS -- history of user-relevant changes
=================================================
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
New in this Isabelle version
----------------------------
*** General ***
* Timeouts for Isabelle/ML tools are subject to system option
"timeout_scale" --- this already used for the overall session build
process before, and allows to adapt to slow machines. The underlying
Timeout.apply in Isabelle/ML treats an original timeout specification 0
as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
in boundary cases.
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
managed via Isabelle/Scala instead of perl; the dependency on
libwww-perl has been eliminated (notably on Linux). Rare
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX).
See also the group "Z Notation" in the Symbols dockable of
Isabelle/jEdit.
*** Isabelle/jEdit Prover IDE ***
* More robust 'proof' outline for method "induct": support nested cases.
* Support for built-in font substitution of jEdit text area.
+* The main plugin for Isabelle/jEdit can be deactivated and reactivated
+as documented --- was broken at least since Isabelle2018.
+
*** Document preparation ***
* More predefined symbols: \ \ (package "stmaryrd"), \ \ (LaTeX package
"pifont").
* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
"pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\.
* Document antiquotations for ML text have been refined: "def" and "ref"
variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
type arguments for constructors (only relevant for index), e.g.
@{ML_type \'a list\} vs. @{ML_type 'a \list\}; @{ML_op} has been renamed
to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax.
* Option "document_logo" determines if an instance of the Isabelle logo
should be created in the document output directory. The given string
specifies the name of the logo variant, while "_" (underscore) refers to
the unnamed variant. The output file name is always "isabelle_logo.pdf".
* Option "document_preprocessor" specifies the name of an executable
that is run within the document output directory, after preparing the
document sources and before the actual build process. This allows to
apply adhoc patches, without requiring a separate "build" script.
* Option "document_build" determines the document build engine, as
defined in Isabelle/Scala (as system service). The subsequent engines
are provided by the Isabelle distribution:
- "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX
- "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
special LaTeX styles)
- "build": delegate to the executable "./build pdf"
The presence of a "build" command within the document output directory
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.
* The command-line tool "isabelle latex" has been discontinued,
INCOMPATIBILITY for old document build scripts.
- Former "isabelle latex -o sty" has become obsolete: Isabelle .sty
files are automatically generated within the document output
directory.
- Former "isabelle latex -o pdf" should be replaced by
"$ISABELLE_LUALATEX root" or "$ISABELLE_PDFLATEX root" (without
quotes), according to the intended LaTeX engine.
- Former "isabelle latex -o bbl" should be replaced by
"$ISABELLE_BIBTEX root" (without quotes).
- Former "isabelle latex -o idx" should be replaced by
"$ISABELLE_MAKEINDEX root" (without quotes).
* Option "document_bibliography" explicitly enables the use of bibtex;
the default is to check the presence of root.bib, but it could have a
different name.
* Improved LaTeX typesetting of \...\ using \guilsinglleft ...
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").
* Simplified typesetting of \...\ using \guillemotleft ...
\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
no longer required.
*** Pure ***
* "global_interpretation" is applicable in instantiation and overloading
targets and in any nested target built on top of a target supporting
"global_interpretation".
*** HOL ***
* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
use explict expression instead. Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
Melem, not_Melem to empty_mset, member_mset, not_member_mset
respectively. Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset": consolidated operation and fact names:
inf_subset_mset ~> inter_mset
sup_subset_mset ~> union_mset
multiset_inter_def ~> inter_mset_def
sup_subset_mset_def ~> union_mset_def
multiset_inter_count ~> count_inter_mset
sup_subset_mset_count ~> count_union_mset
* Theory "HOL-Library.Multiset": syntax precendence for membership
operations has been adjusted to match the corresponding precendences on
sets. Rare INCOMPATIBILITY.
* Theory "HOL-Library.Cardinality": code generator setup based on the
type classes finite_UNIV and card_UNIV has been moved to
"HOL-Library.Code_Cardinality", to avoid incompatibilities with
other code setups for sets in AFP/Containers. Applications relying on
this code setup should import "HOL-Library.Code_Cardinality". Minor
INCOMPATIBILITY.
* Session "HOL-Analysis" and "HOL-Probability": indexed products of
discrete distributions, negative binomial distribution, Hoeffding's
inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
and some more small lemmas. Some theorems that were stated awkwardly
before were corrected. Minor INCOMPATIBILITY.
* Session "HOL-Analysis": the complex Arg function has been identified
with the function "arg" of Complex_Main, renaming arg->Arg also in the
names of arg_bounded. Minor INCOMPATIBILITY.
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
potential for change can be avoided if interpretations of type class
"order" are replaced or augmented by interpretations of locale
"ordering".
* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
INCOMPATIBILITY; note that for most applications less elementary lemmas
exists.
* Theory "HOL-Library.Permutation" has been renamed to the more specific
"HOL-Library.List_Permutation". Note that most notions from that theory
are already present in theory "HOL-Combinatorics.Permutations".
INCOMPATIBILITY.
* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
"Multiset_Permutations", "Perm" have been moved there from session
HOL-Library.
* Theory "HOL-Combinatorics.Transposition" provides elementary swap
operation "transpose".
* Lemma "permutes_induct" has been given stronger hypotheses and named
premises. INCOMPATIBILITY.
* Combinator "Fun.swap" resolved into a mere input abbreviation in
separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
* Bit operations set_bit, unset_bit and flip_bit are now class
operations. INCOMPATIBILITY.
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
"setBit", "clearBit". See there further the changelog in theory Guide.
INCOMPATIBILITY.
* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
INCOMPATIBILITY.
* Sledgehammer:
- Removed legacy "lam_lifting" (synonym for "liftinng") from option
"lam_trans". Minor INCOMPATIBILITY.
- Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
Minor INCOMPATIBILITY.
- Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten
using combinators, but the combinators are kept opaque, i.e. without
definitions.
* Metis:
- Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.
*** ML ***
* ML antiquotations \<^try>\expr\ and \<^can>\expr\ operate directly on
the given ML expression, in contrast to functions "try" and "can" that
modify application of a function.
* ML antiquotations for conditional ML text:
\<^if_linux>\...\
\<^if_macos>\...\
\<^if_windows>\...\
\<^if_unix>\...\
* External bash processes are always managed by Isabelle/Scala, in
contrast to Isabelle2021 where this was only done for macOS on Apple
Silicon.
The main Isabelle/ML interface is Isabelle_System.bash_process with
result type Process_Result.T (resembling class Process_Result in Scala);
derived operations Isabelle_System.bash and Isabelle_System.bash_output
provide similar functionality as before. Rare INCOMPATIBILITY due to
subtle semantic differences:
- Processes invoked from Isabelle/ML actually run in the context of
the Java VM of Isabelle/Scala. The settings environment and current
working directory are usually the same on both sides, but there can be
subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).
- Output via stdout and stderr is line-oriented: Unix vs. Windows
line-endings are normalized towards Unix; presence or absence of a
final newline is irrelevant. The original lines are available as
Process_Result.out_lines/err_lines; the concatenated versions
Process_Result.out/err *omit* a trailing newline (using
Library.trim_line, which was occasional seen in applications before,
but is no longer necessary).
- Output needs to be plain text encoded in UTF-8: Isabelle/Scala
recodes it temporarily as UTF-16. This works for well-formed Unicode
text, but not for arbitrary byte strings. In such cases, the bash
script should write tempory files, managed by Isabelle/ML operations
like Isabelle_System.with_tmp_file to create a file name and
File.read to retrieve its content.
- Just like any other Scala function invoked from ML,
Isabelle_System.bash_process requires a proper PIDE session context.
This could be a regular batch session (e.g. "isabelle build"), a
PIDE editor session (e.g. "isabelle jedit"), or headless PIDE (e.g.
"isabelle dump" or "isabelle server"). Note that old "isabelle
console" or raw "isabelle process" don't have that.
New Process_Result.timing works as in Isabelle/Scala, based on direct
measurements of the bash_process wrapper in C: elapsed time is always
available, CPU time is only available on Linux and macOS, GC time is
unavailable.
* Likewise, the following Isabelle/ML system operations are run in the
context of Isabelle/Scala:
- Isabelle_System.make_directory
- Isabelle_System.copy_dir
- Isabelle_System.copy_file
- Isabelle_System.copy_base_file
- Isabelle_System.rm_tree
- Isabelle_System.download
*** System ***
* ML profiling has been updated and reactivated, after some degration in
Isabelle2021:
- "isabelle build -o threads=1 -o profiling=..." works properly
within the PIDE session context;
- "isabelle profiling_report" now uses the session build database
(like "isabelle log");
- output uses non-intrusive tracing messages, instead of warnings.
* System option "system_log" specifies an optional log file for internal
messages produced by Output.system_message in Isabelle/ML; the value
"true" refers to console progress of the build job. This works for
"isabelle build" or any derivative of it.
* System options of type string may be set to "true" using the short
notation of type bool. E.g. "isabelle build -o system_log".
* System option "document=true" is an alias for "document=pdf" and thus
can be used in the short form. E.g. "isabelle build -o document".
* Command-line tool "isabelle version" supports repository archives
(without full .hg directory). More options.
* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
Note that only Windows supports old 32 bit executables, via settings
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64
(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon).
New in Isabelle2021 (February 2021)
-----------------------------------
*** General ***
* On macOS, the IsabelleXYZ.app directory layout now follows the other
platforms, without indirection via Contents/Resources/. INCOMPATIBILITY,
use e.g. IsabelleXYZ.app/bin/isabelle instead of former
IsabelleXYZ.app/Isabelle/bin/isabelle or
IsabelleXYZ.app/Isabelle/Contents/Resources/IsabelleXYZ/bin/isabelle.
* HTML presentation uses rich markup produced by Isabelle/PIDE,
resulting in more colors and links.
* HTML presentation includes auxiliary files (e.g. ML) for each theory.
* Proof method "subst" is confined to the original subgoal range: its
included distinct_subgoals_tac no longer affects unrelated subgoals.
Rare INCOMPATIBILITY.
* Theory_Data extend operation is obsolete and needs to be the identity
function; merge should be conservative and not reset to the empty value.
Subtle INCOMPATIBILITY and change of semantics (due to
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
the begin of a new theory can be achieved via Theory.at_begin.
*** Isabelle/jEdit Prover IDE ***
* Improved GUI look-and-feel: the portable and scalable "FlatLaf Light"
is used by default on all platforms (appearance similar to IntelliJ
IDEA).
* Improved markup for theory header imports: hyperlinks for theory files
work without formal checking of content.
* The prover process can download auxiliary files (e.g. 'ML_file') for
theories with remote URL. This requires the external "curl" program.
* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
of the formal entity at the caret position.
* The visual feedback on caret entity focus is normally restricted to
definitions within the visible text area. The keyboard modifier "CS"
overrides this: then all defining and referencing positions are shown.
See also option "jedit_focus_modifier".
* The jEdit status line includes widgets both for JVM and ML heap usage.
Ongoing ML ongoing garbage collection is shown as "ML cleanup".
* The Monitor dockable provides buttons to request a full garbage
collection and sharing of live data on the ML heap. It also includes
information about the Java Runtime system.
* PIDE support for session ROOTS: markup for directories.
* Update to jedit-5.6.0, the latest release. This version works properly
on macOS by default, without the special MacOSX plugin.
* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
for better approximate window size on macOS and Linux/X11.
* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode,
but non-native look-and-feel (FlatLaf).
* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
viewer, instead of re-using the jEdit text editor.
* IDE support for Naproche-SAD: Proof Checking of Natural Mathematical
Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
.ftl.tex extension. The corresponding Naproche-SAD server process can be
disabled by setting the system option naproche_server=false and
restarting the Isabelle application.
*** Document preparation ***
* Keyword 'document_theories' within ROOT specifies theories from other
sessions that should be included in the generated document source
directory. This does not affect the generated session.tex: \input{...}
needs to be used separately.
* The standard LaTeX engine is now lualatex, according to settings
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
pdflatex, but text encoding needs to conform strictly to utf8. Rare
INCOMPATIBILITY.
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
document output is always PDF.
* Antiquotation @{tool} refers to Isabelle command-line tools, with
completion and formal reference to the source (external script or
internal Scala function).
* Antiquotation @{bash_function} refers to GNU bash functions that are
checked within the Isabelle settings environment.
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
@{scala_method} refer to checked Isabelle/Scala entities.
*** Pure ***
* Session Pure-Examples contains notable examples for Isabelle/Pure
(former entries of HOL-Isar_Examples).
* Named contexts (locale and class specifications, locale and class
context blocks) allow bundle mixins for the surface context. This allows
syntax notations to be organized within bundles conveniently. See theory
"HOL-ex.Specifications_with_bundle_mixins" for examples and the isar-ref
manual for syntax descriptions.
* Definitions in locales produce rule which can be added as congruence
rule to protect foundational terms during simplification.
* Consolidated terminology and function signatures for nested targets:
- Local_Theory.begin_nested replaces Local_Theory.open_target
- Local_Theory.end_nested replaces Local_Theory.close_target
- Combination of Local_Theory.begin_nested and
Local_Theory.end_nested(_result) replaces
Local_Theory.subtarget(_result)
INCOMPATIBILITY.
* Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY.
*** HOL ***
* Session HOL-Examples contains notable examples for Isabelle/HOL
(former entries of HOL-Isar_Examples, HOL-ex etc.).
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
HOL-Word-SMT_Examples.
* Zipperposition 2.0 is now included as Isabelle component for
experimentation, e.g. in "sledgehammer [prover = zipperposition]".
* Sledgehammer:
- support veriT in proof preplay
- take adventage of more cores in proof preplay
* Updated the Metis prover underlying the "metis" proof method to
version 2.4 (release 20180810). The new version fixes one soundness
defect and two incompleteness defects. Very slight INCOMPATIBILITY.
* Nitpick/Kodkod may be invoked directly within the running
Isabelle/Scala session (instead of an external Java process): this
improves reactivity and saves resources. This experimental feature is
guarded by system option "kodkod_scala" (default: true in PIDE
interaction, false in batch builds).
* Simproc "defined_all" and rewrite rule "subst_all" perform more
aggressive substitution with variables from assumptions.
INCOMPATIBILITY, consider repairing proofs locally like this:
supply subst_all [simp del] [[simproc del: defined_all]]
* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
on datatypes to "False" if either side is a proper subexpression of the
other (for any datatype with a reasonable size function).
* Syntax for state monad combinators fcomp and scomp is organized in
bundle state_combinator_syntax. Minor INCOMPATIBILITY.
* Syntax for reflected term syntax is organized in bundle term_syntax,
discontinuing previous locale term_syntax. Minor INCOMPATIBILITY.
* New constant "power_int" for exponentiation with integer exponent,
written as "x powi n".
* Added the "at most 1" quantifier, Uniq.
* For the natural numbers, "Sup {} = 0".
* New constant semiring_char gives the characteristic of any type of
class semiring_1, with the convenient notation CHAR('a). For example,
CHAR(nat) = CHAR(int) = CHAR(real) = 0, CHAR(17) = 17.
* HOL-Computational_Algebra.Polynomial: Definition and basic properties
of algebraic integers.
* Library theory "Bit_Operations" with generic bit operations.
* Library theory "Signed_Division" provides operations for signed
division, instantiated for type int.
* Theory "Multiset": removed misleading notation \# for sum_mset;
replaced with \\<^sub>#. Analogous notation for prod_mset also exists now.
* New theory "HOL-Library.Word" takes over material from former session
"HOL-Word". INCOMPATIBILITY: need to adjust imports.
* Theory "HOL-Library.Word": Type word is restricted to bit strings
consisting of at least one bit. INCOMPATIBILITY.
* Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based
on generic algebraic bit operations from theory
"HOL-Library.Bit_Operations". INCOMPATIBILITY.
* Theory "HOL-Library.Word": Most operations on type word are set up for
transfer and lifting. INCOMPATIBILITY.
* Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY,
sometimes additional rewrite rules must be added to applications to get
a confluent system again.
* Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for
both types int and word. INCOMPATIBILITY.
* Theory "HOL-Library.Word": Syntax for signed compare operators has
been consolidated with syntax of regular compare operators. Minor
INCOMPATIBILITY.
* Former session "HOL-Word": Various operations dealing with bit values
represented as reversed lists of bools are separated into theory
Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.
* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.
* Former session "HOL-Word": Compound operation "bin_split" simplifies
by default into its components "drop_bit" and "take_bit".
INCOMPATIBILITY.
* Former session "HOL-Word": Operations lsb, msb and set_bit are
separated into theories Least_significant_bit, Most_significant_bit and
Generic_set_bit respectively in session Word_Lib in the AFP.
INCOMPATIBILITY.
* Former session "HOL-Word": Ancient int numeral representation has been
factored out in separate theory "Ancient_Numeral" in session Word_Lib in
the AFP. INCOMPATIBILITY.
* Former session "HOL-Word": Operations "bin_last", "bin_rest",
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
"max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.
* Former session "HOL-Word": Misc ancient material has been factored out
into separate theories and moved to session Word_Lib in the AFP. See
theory "Guide" there for further information. INCOMPATIBILITY.
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
are in working order again, as opposed to outputting "GaveUp" on nearly
all problems.
* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
abstract language constructors.
* Session "HOL-Hoare": now provides a total correctness logic as well.
*** FOL ***
* Added the "at most 1" quantifier, Uniq, as in HOL.
* Simproc "defined_all" and rewrite rule "subst_all" have been changed
as in HOL.
*** ML ***
* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
registered Isabelle/Scala functions (of type String => String):
invocation works via the PIDE protocol.
* Path.append is available as overloaded "+" operator, similar to
corresponding Isabelle/Scala operation.
* ML statistics via an external Poly/ML process: this allows monitoring
the runtime system while the ML program sleeps.
*** System ***
* Isabelle server allows user-defined commands via
isabelle_scala_service.
* Update/rebuild external provers on currently supported OS platforms,
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
* The command-line tool "isabelle log" prints prover messages from the
build database of the given session, following the the order of theory
sources, instead of erratic parallel evaluation. Consequently, the
session log file is restricted to system messages of the overall build
process, and thus becomes more informative.
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
variable.
* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
(for DVI documents) has been discontinued. Former option -n has been
turned into -o with explicit file name. Minor INCOMPATIBILITY.
* The command-line tool "isabelle components" supports new options -u
and -x to manage $ISABELLE_HOME_USER/etc/components without manual
editing of Isabelle configuration files.
* The shell function "isabelle_directory" (within etc/settings of
components) augments the list of special directories for persistent
symbolic path names. This improves portability of heap images and
session databases. It used to be hard-wired for Isabelle + AFP, but
other projects may now participate on equal terms.
* The command-line tool "isabelle process" now prints output to
stdout/stderr separately and incrementally, instead of just one bulk to
stdout after termination. Potential INCOMPATIBILITY for external tools.
* The command-line tool "isabelle console" now supports interrupts
properly (on Linux and macOS).
* Batch-builds via "isabelle build" use a PIDE session with special
protocol: this allows to invoke Isabelle/Scala operations from
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
This includes full PIDE markup, if option "build_pide_reports" is
enabled.
* The command-line tool "isabelle build" provides option -P DIR to
produce PDF/HTML presentation in the specified directory; -P: refers to
the standard directory according to ISABELLE_BROWSER_INFO /
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken
from the build database -- from this or earlier builds with option
document=pdf.
* The command-line tool "isabelle document" generates theory documents
on the spot, using the underlying session build database (exported
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former
"isabelle document" tool was rather different and has been discontinued.
* The command-line tool "isabelle sessions" explores the structure of
Isabelle sessions and prints result names in topological order (on
stdout).
* The Isabelle/Scala "Progress" interface changed slightly and
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
instead.
* General support for Isabelle/Scala system services, configured via the
shell function "isabelle_scala_service" in etc/settings (e.g. of an
Isabelle component); see implementations of class
Isabelle_System.Service in Isabelle/Scala. This supersedes former
"isabelle_scala_tools" and "isabelle_file_format": minor
INCOMPATIBILITY.
* The syntax of theory load commands (for auxiliary files) is now
specified in Isabelle/Scala, as instance of class
isabelle.Command_Span.Load_Command registered via isabelle_scala_service
in etc/settings. This allows more flexible schemes than just a list of
file extensions. Minor INCOMPATIBILITY, e.g. see theory
HOL-SPARK.SPARK_Setup to emulate the old behaviour.
* JVM system property "isabelle.laf" has been discontinued; the default
Swing look-and-feel is ""FlatLaf Light".
* Isabelle/Phabricator supports Ubuntu 20.04 LTS.
* Isabelle/Phabricator setup has been updated to follow ongoing
development: libphutil has been discontinued. Minor INCOMPATIBILITY:
existing server installations should remove libphutil from
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
directory (e.g. /var/www/phabricator-vcs/libphutil).
* Experimental support for arm64-linux platform. The reference platform
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
* Support for Apple Silicon, using mostly x86_64-darwin runtime
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
some native arm64-darwin executables (e.g. Java).
New in Isabelle2020 (April 2020)
--------------------------------
*** General ***
* Session ROOT files need to specify explicit 'directories' for import
of theory files. Directories cannot be shared by different sessions.
(Recall that import of theories from other sessions works via
session-qualified theory names, together with suitable 'sessions'
declarations in the ROOT.)
* Internal derivations record dependencies on oracles and other theorems
accurately, including the implicit type-class reasoning wrt. proven
class relations and type arities. In particular, the formal tagging with
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
propagated properly to theorems depending on such type instances.
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
actual proposition that is assumed in the goal and proof context. This
requires at least Proofterm.proofs = 1 to show up in theorem
dependencies.
* Command 'thm_oracles' prints all oracles used in given theorems,
covering the full graph of transitive dependencies.
* Command 'thm_deps' prints immediate theorem dependencies of the given
facts. The former graph visualization has been discontinued, because it
was hardly usable.
* Refined treatment of proof terms, including type-class proofs for
minor object-logics (FOL, FOLP, Sequents).
* The inference kernel is now confined to one main module: structure
Thm, without the former circular dependency on structure Axclass.
* Mixfix annotations may use "' " (single quote followed by space) to
separate delimiters (as documented in the isar-ref manual), without
requiring an auxiliary empty block. A literal single quote needs to be
escaped properly. Minor INCOMPATIBILITY.
*** Isar ***
* The proof method combinator (subproofs m) applies the method
expression m consecutively to each subgoal, constructing individual
subproofs internally. This impacts the internal construction of proof
terms: it makes a cascade of let-expressions within the derivation tree
and may thus improve scalability.
* Attribute "trace_locales" activates tracing of locale instances during
roundup. It replaces the diagnostic command 'print_dependencies', which
has been discontinued.
*** Isabelle/jEdit Prover IDE ***
* Prover IDE startup is now much faster, because theory dependencies are
no longer explored in advance. The overall session structure with its
declarations of 'directories' is sufficient to locate theory files. Thus
the "session focus" of option "isabelle jedit -S" has become obsolete
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
sufficient and more convenient to start editing a particular session.
* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
tooltip message popups, corresponding to mouse hovering with/without the
CONTROL/COMMAND key pressed.
* The following actions allow to navigate errors within the current
document snapshot:
isabelle.first-error (CS+a)
isabelle.last-error (CS+z)
isabelle.next-error (CS+n)
isabelle.prev-error (CS+p)
* Support more brackets: \ \ (intended for implicit argument syntax).
* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
Monitor) applies the jconsole tool on the running Isabelle/jEdit
process. This allows to monitor resource usage etc.
* More adequate default font sizes for Linux on HD / UHD displays:
automatic font scaling is usually absent on Linux, in contrast to
Windows and macOS.
* The default value for the jEdit property "view.antiAlias" (menu item
Utilities / Global Options / Text Area / Anti Aliased smooth text) is
now "subpixel HRGB", instead of former "standard". Especially on Linux
this often leads to faster text rendering, but can also cause problems
with odd color shades. An alternative is to switch back to "standard"
here, and set the following Java system property:
isabelle jedit -Dsun.java2d.opengl=true
This can be made persistent via JEDIT_JAVA_OPTIONS in
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
application there is a corresponding options file in the same directory.
*** Isabelle/VSCode Prover IDE ***
* Update of State and Preview panels to use new WebviewPanel API of
VSCode.
*** HOL ***
* Improvements of the 'lift_bnf' command:
- Add support for quotient types.
- Generate transfer rules for the lifted map/set/rel/pred constants
(theorems "._transfer_raw").
* Term_XML.Encode/Decode.term uses compact representation of Const
"typargs" from the given declaration environment. This also makes more
sense for translations to lambda-calculi with explicit polymorphism.
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
applications.
* ASCII membership syntax concerning big operators for infimum and
supremum has been discontinued. INCOMPATIBILITY.
* Removed multiplicativity assumption from class
"normalization_semidom". Introduced various new intermediate classes
with the multiplicativity assumption; many theorem statements
(especially involving GCD/LCM) had to be adapted. This allows for a more
natural instantiation of the algebraic typeclasses for e.g. Gaussian
integers. INCOMPATIBILITY.
* Clear distinction between types for bits (False / True) and Z2 (0 /
1): theory HOL-Library.Bit has been renamed accordingly.
INCOMPATIBILITY.
* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
to algebra_simps and field_simps but contain more aggressive rules
potentially splitting goals; algebra_split_simps roughly replaces
sign_simps and field_split_simps can be used instead of divide_simps.
INCOMPATIBILITY.
* Theory HOL.Complete_Lattices:
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\)
associates to the left now as is customary.
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
multiple colours and arbitrary exponents.
* Session HOL-Proofs: build faster thanks to better treatment of proof
terms in Isabelle/Pure.
* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
INCOMPATIBILITY.
* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.
* Session HOL-Complex_Analysis has been split off from HOL-Analysis.
*** ML ***
* Theory construction may be forked internally, the operation
Theory.join_theory recovers a single result theory. See also the example
in theory "HOL-ex.Join_Theory".
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
* Minimal support for a soft-type system within the Isabelle logical
framework (module Soft_Type_System).
* Former Variable.auto_fixes has been replaced by slightly more general
Proof_Context.augment: it is subject to an optional soft-type system of
the underlying object-logic. Minor INCOMPATIBILITY.
* More scalable Export.export using XML.tree to avoid premature string
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.
* Prover IDE support for the underlying Poly/ML compiler (not the basis
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
implementation with full markup.
*** System ***
* Standard rendering for more Isabelle symbols: \ \ \ \
* The command-line tool "isabelle scala_project" creates a Gradle
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
such as IntelliJ IDEA.
* The command-line tool "isabelle phabricator_setup" facilitates
self-hosting of the Phabricator software-development platform, with
support for Git, Mercurial, Subversion repositories. This helps to avoid
monoculture and to escape the gravity of centralized version control by
Github and/or Bitbucket. For further documentation, see chapter
"Phabricator server administration" in the "system" manual. A notable
example installation is https://isabelle-dev.sketis.net/.
* The command-line tool "isabelle hg_setup" simplifies the setup of
Mercurial repositories, with hosting via Phabricator or SSH file server
access.
* The command-line tool "isabelle imports" has been discontinued: strict
checking of session directories enforces session-qualified theory names
in applications -- users are responsible to specify session ROOT entries
properly.
* The command-line tool "isabelle dump" and its underlying
Isabelle/Scala module isabelle.Dump has become more scalable, by
splitting sessions and supporting a base logic image. Minor
INCOMPATIBILITY in options and parameters.
* The command-line tool "isabelle build_docker" has been slightly
improved: it is now properly documented in the "system" manual.
* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
users, system services.
* Isabelle/Scala support for proof terms (with full type/term
information) in module isabelle.Term.
* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
"isabelle dump".
* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
exported as well: this spans an overall dependency graph of internal
inferences; it might help to reconstruct the formal structure of theory
libraries. See also the module isabelle.Export_Theory in Isabelle/Scala.
* Theory export of structured specifications, based on internal
declarations of Spec_Rules by packages like 'definition', 'inductive',
'primrec', 'function'.
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
have been discontinued -- deprecated since Isabelle2018.
* More complete x86_64 platform support on macOS, notably Catalina where
old x86 has been discontinued.
* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.
* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).
New in Isabelle2019 (June 2019)
-------------------------------
*** General ***
* The font collection "Isabelle DejaVu" is systematically derived from
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges and
augmented by special Isabelle symbols, taken from the former
"IsabelleText" font (which is no longer provided separately). The line
metrics and overall rendering quality is closer to original DejaVu.
INCOMPATIBILITY with display configuration expecting the old
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.
* The Isabelle fonts render "\" properly as superscript "-1".
* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).
* Old-style {* verbatim *} tokens are explicitly marked as legacy
feature and will be removed soon. Use \cartouche\ syntax instead, e.g.
via "isabelle update_cartouches -t" (available since Isabelle2015).
* Infix operators that begin or end with a "*" are now parenthesized
without additional spaces, e.g. "(*)" instead of "( * )". Minor
INCOMPATIBILITY.
* Mixfix annotations may use cartouches instead of old-style double
quotes, e.g. (infixl \+\ 60). The command-line tool "isabelle update -u
mixfix_cartouches" allows to update existing theory sources
automatically.
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
need to provide a closed expression -- without trailing semicolon. Minor
INCOMPATIBILITY.
* Commands 'generate_file', 'export_generated_files', and
'compile_generated_files' support a stateless (PIDE-conformant) model
for generated sources and compiled binaries of other languages. The
compilation process is managed in Isabelle/ML, and results exported to
the session database for further use (e.g. with "isabelle export" or
"isabelle build -e").
*** Isabelle/jEdit Prover IDE ***
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. Line spacing no longer needs to be
adjusted: properties for the old IsabelleText font had "Global Options /
Text Area / Extra vertical line spacing (in pixels): -2", it now
defaults to 1, but 0 works as well.
* The jEdit File Browser is more prominent in the default GUI layout of
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
resources, notably via "favorites:" (or "Edit Favorites").
* Further markup and rendering for "plain text" (e.g. informal prose)
and "raw text" (e.g. verbatim sources). This improves the visual
appearance of formal comments inside the term language, or in general
for repeated alternation of formal and informal text.
* Action "isabelle-export-browser" points the File Browser to the theory
exports of the current buffer, based on the "isabelle-export:" virtual
file-system. The directory view needs to be reloaded manually to follow
ongoing document processing.
* Action "isabelle-session-browser" points the File Browser to session
information, based on the "isabelle-session:" virtual file-system. Its
entries are structured according to chapter / session names, the open
operation is redirected to the session ROOT file.
* Support for user-defined file-formats via class isabelle.File_Format
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
the shell function "isabelle_file_format" in etc/settings (e.g. of an
Isabelle component).
* System option "jedit_text_overview" allows to disable the text
overview column.
* Command-line options "-s" and "-u" of "isabelle jedit" override the
default for system option "system_heaps" that determines the heap
storage directory for "isabelle build". Option "-n" is now clearly
separated from option "-s".
* The Isabelle/jEdit desktop application uses the same options as
"isabelle jedit" for its internal "isabelle build" process: the implicit
option "-o system_heaps" (or "-s") has been discontinued. This reduces
the potential for surprise wrt. command-line tools.
* The official download of the Isabelle/jEdit application already
contains heap images for Isabelle/HOL within its main directory: thus
the first encounter becomes faster and more robust (e.g. when run from a
read-only directory).
* Isabelle DejaVu fonts are available with hinting by default, which is
relevant for low-resolution displays. This may be disabled via system
option "isabelle_fonts_hinted = false" in
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
results.
* OpenJDK 11 has quite different font rendering, with better glyph
shapes and improved sub-pixel anti-aliasing. In some situations results
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
display is recommended.
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
property jdk.gtk.version). The factory default is version 3, but
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
this more conservative (as in Java 8). Depending on the GTK theme
configuration, "-Djdk.gtk.version=3" might work better or worse.
*** Document preparation ***
* Document markers are formal comments of the form \<^marker>\marker_body\ that
are stripped from document output: the effect is to modify the semantic
presentation context or to emit markup to the PIDE document. Some
predefined markers are taken from the Dublin Core Metadata Initiative,
e.g. \<^marker>\contributor arg\ or \<^marker>\license arg\ and produce PIDE markup that
can be retrieved from the document database.
* Old-style command tags %name are re-interpreted as markers with
proof-scope \<^marker>\tag (proof) name\ and produce LaTeX environments as
before. Potential INCOMPATIBILITY: multiple markers are composed in
canonical order, resulting in a reversed list of tags in the
presentation context.
* Marker \<^marker>\tag name\ does not apply to the proof of a top-level goal
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
of semantics wrt. old-style %name.
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\tag \"
template.
* Document antiquotation option "cartouche" indicates if the output
should be delimited as cartouche; this takes precedence over the
analogous option "quotes".
* Many document antiquotations are internally categorized as "embedded"
and expect one cartouche argument, which is typically used with the
\<^control>\cartouche\ notation (e.g. \<^term>\\x y. x\). The cartouche
delimiters are stripped in output of the source (antiquotation option
"source"), but it is possible to enforce delimiters via option
"source_cartouche", e.g. @{term [source_cartouche] \\x y. x\}.
*** Isar ***
* Implicit cases goal1, goal2, goal3, etc. have been discontinued
(legacy feature since Isabelle2016).
* More robust treatment of structural errors: begin/end blocks take
precedence over goal/proof. This is particularly relevant for the
headless PIDE session and server.
* Command keywords of kind thy_decl / thy_goal may be more specifically
fit into the traditional document model of "definition-statement-proof"
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.
*** HOL ***
* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
provides a virtual file-system "isabelle-export:" that can be explored
in the regular file-browser. A 'file_prefix' argument allows to specify
an explicit name prefix for the target file (SML, OCaml, Scala) or
directory (Haskell); the default is "export" with a consecutive number
within each theory.
* Command 'export_code': the 'file' argument is now legacy and will be
removed soon: writing to the physical file-system is not well-defined in
a reactive/parallel application like Isabelle. The empty 'file' argument
has been discontinued already: it is superseded by the file-browser in
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
* Command 'code_reflect' no longer supports the 'file' argument: it has
been superseded by 'file_prefix' for stateless file management as in
'export_code'. Minor INCOMPATIBILITY.
* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.
* Code generation for OCaml: Zarith supersedes Nums as library for
proper integer arithmetic. The library is located via standard
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
The environment provided by "isabelle ocaml_setup" already contains this
tool and the required packages. Minor INCOMPATIBILITY.
* Code generation for Haskell: code includes for Haskell must contain
proper module frame, nothing is added magically any longer.
INCOMPATIBILITY.
* Code generation: slightly more conventional syntax for 'code_stmts'
antiquotation. Minor INCOMPATIBILITY.
* Theory List: the precedence of the list_update operator has changed:
"f a [n := x]" now needs to be written "(f a)[n := x]".
* The functions \, \, \, \ (not the corresponding binding operators)
now have the same precedence as any other prefix function symbol. Minor
INCOMPATIBILITY.
* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer
and need to be given explicitly. Auxiliary abbreviations INFIMUM,
SUPREMUM, UNION, INTER should now rarely occur in output and are just
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
are gone INCOMPATIBILITY.
* The simplifier uses image_cong_simp as a congruence rule. The historic
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
not used by default any longer. INCOMPATIBILITY; consider using declare
image_cong_simp [cong del] in extreme situations.
* INF_image and SUP_image are no default simp rules any longer.
INCOMPATIBILITY, prefer image_comp as simp rule if needed.
* Strong congruence rules (with =simp=> in the premises) for constant f
are now uniformly called f_cong_simp, in accordance with congruence
rules produced for mappers by the datatype package. INCOMPATIBILITY.
* Retired lemma card_Union_image; use the simpler card_UN_disjoint
instead. INCOMPATIBILITY.
* Facts sum_mset.commute and prod_mset.commute have been renamed to
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.
* ML structure Inductive: slightly more conventional naming schema.
Minor INCOMPATIBILITY.
* ML: Various _global variants of specification tools have been removed.
Minor INCOMPATIBILITY, prefer combinators
Named_Target.theory_map[_result] to lift specifications to the global
theory level.
* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
overlapping and non-exhaustive patterns and handles arbitrarily nested
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
assumes sequential left-to-right pattern matching. The generated
equation no longer tuples the arguments on the right-hand side.
INCOMPATIBILITY.
* Theory HOL-Library.Multiset: the \# operator now has the same
precedence as any other prefix function symbol.
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
of the bundle cardinal_syntax (available in theory Main). Minor
INCOMPATIBILITY.
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
used for computing powers in class "monoid_mult" and modular
exponentiation.
* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
of Formal power series.
* Session HOL-Number_Theory: More material on residue rings in
Carmichael's function, primitive roots, more properties for "ord".
* Session HOL-Analysis: Better organization and much more material
at the level of abstract topological spaces.
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
algebraic closure of a field by de Vilhena and Baillon.
* Session HOL-Homology has been added. It is a port of HOL Light's
homology library, with new proofs of "invariance of domain" and related
results.
* Session HOL-SPARK: .prv files are no longer written to the
file-system, but exported to the session database. Results may be
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
command-line.
* Sledgehammer:
- The URL for SystemOnTPTP, which is used by remote provers, has been
updated.
- The machine-learning-based filter MaSh has been optimized to take
less time (in most cases).
* SMT: reconstruction is now possible using the SMT solver veriT.
* Session HOL-Word:
* New theory More_Word as comprehensive entrance point.
* Merged type class bitss into type class bits.
INCOMPATIBILITY.
*** ML ***
* Command 'generate_file' allows to produce sources for other languages,
with antiquotations in the Isabelle context (only the control-cartouche
form). The default "cartouche" antiquotation evaluates an ML expression
of type string and inlines the result as a string literal of the target
language. For example, this works for Haskell as follows:
generate_file "Pure.hs" = \
module Isabelle.Pure where
allConst, impConst, eqConst :: String
allConst = \\<^const_name>\Pure.all\\
impConst = \\<^const_name>\Pure.imp\\
eqConst = \\<^const_name>\Pure.eq\\
\
See also commands 'export_generated_files' and 'compile_generated_files'
to use the results.
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for Isabelle/ML, or "SML" for official Standard ML.
* ML antiquotation @{master_dir} refers to the master directory of the
underlying theory, i.e. the directory of the theory file.
* ML antiquotation @{verbatim} inlines its argument as string literal,
preserving newlines literally. The short form \<^verbatim>\abc\ is particularly
useful.
* Local_Theory.reset is no longer available in user space. Regular
definitional packages should use balanced blocks of
Local_Theory.open_target versus Local_Theory.close_target instead, or
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").
*** System ***
* Update to OpenJDK 11: the current long-term support version of Java.
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.
* System option "checkpoint" has been discontinued: obsolete thanks to
improved memory management in Poly/ML.
* System option "system_heaps" determines where to store the session
image of "isabelle build" (and other tools using that internally).
Former option "-s" is superseded by option "-o system_heaps".
INCOMPATIBILITY in command-line syntax.
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
source modules for Isabelle tools implemented in Haskell, notably for
Isabelle/PIDE.
* The command-line tool "isabelle build -e" retrieves theory exports
from the session build database, using 'export_files' in session ROOT
entries.
* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
section "Theory update". Theory sessions are specified as in "isabelle
dump".
* The command-line tool "isabelle update -u control_cartouches" changes
antiquotations into control-symbol format (where possible): @{NAME}
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\ARG\.
* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).
* Isabelle Server command "use_theories" supports "nodes_status_delay"
for continuous output of node status information. The time interval is
specified in seconds; a negative value means it is disabled (default).
* Isabelle Server command "use_theories" terminates more robustly in the
presence of structurally broken sources: full consolidation of theories
is no longer required.
* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
which needs to point to a suitable version of "ocamlfind" (e.g. via
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
ISABELLE_OCAMLC are no longer supported.
* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:
isabelle ghc_setup
isabelle ghc_stack
isabelle ocaml_setup
isabelle ocaml_opam
The global installation state is determined by the following settings
(and corresponding directory contents):
ISABELLE_STACK_ROOT
ISABELLE_STACK_RESOLVER
ISABELLE_GHC_VERSION
ISABELLE_OPAM_ROOT
ISABELLE_OCAML_VERSION
After setup, the following Isabelle settings are automatically
redirected (overriding existing user settings):
ISABELLE_GHC
ISABELLE_OCAMLFIND
The old meaning of these settings as locally installed executables may
be recovered by purging the directories ISABELLE_STACK_ROOT /
ISABELLE_OPAM_ROOT, or by resetting these variables in
$ISABELLE_HOME_USER/etc/settings.
New in Isabelle2018 (August 2018)
---------------------------------
*** General ***
* Session-qualified theory names are mandatory: it is no longer possible
to refer to unqualified theories from the parent session.
INCOMPATIBILITY for old developments that have not been updated to
Isabelle2017 yet (using the "isabelle imports" tool).
* Only the most fundamental theory names are global, usually the entry
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
* Global facts need to be closed: no free variables and no hypotheses.
Rare INCOMPATIBILITY.
* Facts stemming from locale interpretation are subject to lazy
evaluation for improved performance. Rare INCOMPATIBILITY: errors
stemming from interpretation morphisms might be deferred and thus
difficult to locate; enable system option "strict_facts" temporarily to
avoid this.
* Marginal comments need to be written exclusively in the new-style form
"\ \text\", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle
update_comments" to update existing theory files.
* Old-style inner comments (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "\ \...\" or "\<^cancel>\...\"
instead.
* The "op " syntax for infix operators has been replaced by
"()". If begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.
INCOMPATIBILITY, use the command-line tool "isabelle update_op" to
convert theory and ML files to the new syntax. Because it is based on
regular expression matching, the result may need a bit of manual
postprocessing. Invoking "isabelle update_op" converts all files in the
current directory (recursively). In case you want to exclude conversion
of ML files (because the tool frequently also converts ML's "op"
syntax), use option "-m".
* Theory header 'abbrevs' specifications need to be separated by 'and'.
INCOMPATIBILITY.
* Command 'external_file' declares the formal dependency on the given
file name, such that the Isabelle build process knows about it, but
without specific Prover IDE management.
* Session ROOT entries no longer allow specification of 'files'. Rare
INCOMPATIBILITY, use command 'external_file' within a proper theory
context.
* Session root directories may be specified multiple times: each
accessible ROOT file is processed only once. This facilitates
specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
-d or -D for "isabelle build" and "isabelle jedit". Example:
isabelle build -D '~~/src/ZF'
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.
* In HTML output, the Isabelle symbol "\" is rendered as explicit
Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML
output.
*** Isabelle/jEdit Prover IDE ***
* The command-line tool "isabelle jedit" provides more flexible options
for session management:
- option -R builds an auxiliary logic image with all theories from
other sessions that are not already present in its parent
- option -S is like -R, with a focus on the selected session and its
descendants (this reduces startup time for big projects like AFP)
- option -A specifies an alternative ancestor session for options -R
and -S
- option -i includes additional sessions into the name-space of
theories
Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
* PIDE markup for session ROOT files: allows to complete session names,
follow links to theories and document files etc.
* Completion supports theory header imports, using theory base name.
E.g. "Prob" may be completed to "HOL-Probability.Probability".
* Named control symbols (without special Unicode rendering) are shown as
bold-italic keyword. This is particularly useful for the short form of
antiquotations with control symbol: \<^name>\argument\. The action
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
arguments into this format.
* Completion provides templates for named symbols with arguments,
e.g. "\ \ARGUMENT\" or "\<^emph>\ARGUMENT\".
* Slightly more parallel checking, notably for high priority print
functions (e.g. State output).
* The view title is set dynamically, according to the Isabelle
distribution and the logic session name. The user can override this via
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).
* System options "spell_checker_include" and "spell_checker_exclude"
supersede former "spell_checker_elements" to determine regions of text
that are subject to spell-checking. Minor INCOMPATIBILITY.
* Action "isabelle.preview" is able to present more file formats,
notably bibtex database files and ML files.
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
plain-text document draft. Both are available via the menu "Plugins /
Isabelle".
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
is only used if there is no conflict with existing Unicode sequences in
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle
symbols remain in literal \ form. This avoids accidental loss of
Unicode content when saving the file.
* Bibtex database files (.bib) are semantically checked.
* Update to jedit-5.5.0, the latest release.
*** Isabelle/VSCode Prover IDE ***
* HTML preview of theories and other file-formats similar to
Isabelle/jEdit.
* Command-line tool "isabelle vscode_server" accepts the same options
-A, -R, -S, -i for session selection as "isabelle jedit". This is
relevant for isabelle.args configuration settings in VSCode. The former
option -A (explore all known session files) has been discontinued: it is
enabled by default, unless option -S is used to focus on a particular
spot in the session structure. INCOMPATIBILITY.
*** Document preparation ***
* Formal comments work uniformly in outer syntax, inner syntax (term
language), Isabelle/ML and some other embedded languages of Isabelle.
See also "Document comments" in the isar-ref manual. The following forms
are supported:
- marginal text comment: \ \\\
- canceled source: \<^cancel>\\\
- raw LaTeX: \<^latex>\\\
* Outside of the inner theory body, the default presentation context is
theory Pure. Thus elementary antiquotations may be used in markup
commands (e.g. 'chapter', 'section', 'text') and formal comments.
* System option "document_tags" specifies alternative command tags. This
is occasionally useful to control the global visibility of commands via
session options (e.g. in ROOT).
* Document markup commands ('section', 'text' etc.) are implicitly
tagged as "document" and visible by default. This avoids the application
of option "document_tags" to these commands.
* Isabelle names are mangled into LaTeX macro names to allow the full
identifier syntax with underscore, prime, digits. This is relevant for
antiquotations in control symbol notation, e.g. \<^const_name> becomes
\isactrlconstUNDERSCOREname.
* Document preparation with skip_proofs option now preserves the content
more accurately: only terminal proof steps ('by' etc.) are skipped.
* Document antiquotation @{theory name} requires the long
session-qualified theory name: this is what users reading the text
normally need to import.
* Document antiquotation @{session name} checks and prints the given
session name verbatim.
* Document antiquotation @{cite} now checks the given Bibtex entries
against the Bibtex database files -- only in batch-mode session builds.
* Command-line tool "isabelle document" has been re-implemented in
Isabelle/Scala, with simplified arguments and explicit errors from the
latex and bibtex process. Minor INCOMPATIBILITY.
* Session ROOT entry: empty 'document_files' means there is no document
for this session. There is no need to specify options [document = false]
anymore.
*** Isar ***
* Command 'interpret' no longer exposes resulting theorems as literal
facts, notably for the \prop\ notation or the "fact" proof method. This
improves modularity of proofs and scalability of locale interpretation.
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
(e.g. use 'find_theorems' or 'try' to figure this out).
* The old 'def' command has been discontinued (legacy since
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.
*** Pure ***
* The inner syntax category "sort" now includes notation "_" for the
dummy sort: it is effectively ignored in type-inference.
* Rewrites clauses (keyword 'rewrites') were moved into the locale
expression syntax, where they are part of locale instances. In
interpretation commands rewrites clauses now need to occur before 'for'
and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to
rewriting may need to be pulled up into the surrounding theory.
* For 'rewrites' clauses, if activating a locale instance fails, fall
back to reading the clause first. This helps avoid qualification of
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.
* Proof method "simp" now supports a new modifier "flip:" followed by a
list of theorems. Each of these theorems is removed from the simpset
(without warning if it is not there) and the symmetric version of the
theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto"
and friends the modifier is "simp flip:".
*** HOL ***
* Sledgehammer: bundled version of "vampire" (for non-commercial users)
helps to avoid fragility of "remote_vampire" service.
* Clarified relationship of characters, strings and code generation:
- Type "char" is now a proper datatype of 8-bit values.
- Conversions "nat_of_char" and "char_of_nat" are gone; use more
general conversions "of_char" and "char_of" with suitable type
constraints instead.
- The zero character is just written "CHR 0x00", not "0" any longer.
- Type "String.literal" (for code generation) is now isomorphic to
lists of 7-bit (ASCII) values; concrete values can be written as
"STR ''...''" for sequences of printable characters and "STR 0x..."
for one single ASCII code point given as hexadecimal numeral.
- Type "String.literal" supports concatenation "... + ..." for all
standard target languages.
- Theory HOL-Library.Code_Char is gone; study the explanations
concerning "String.literal" in the tutorial on code generation to
get an idea how target-language string literals can be converted to
HOL string values and vice versa.
- Session Imperative-HOL: operation "raise" directly takes a value of
type "String.literal" as argument, not type "string".
INCOMPATIBILITY.
* Code generation: Code generation takes an explicit option
"case_insensitive" to accomodate case-insensitive file systems.
* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.
* New, more general, axiomatization of complete_distrib_lattice. The
former axioms:
"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
are replaced by:
"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \ A . f Y \ Y)})"
The instantiations of sets and functions as complete_distrib_lattice are
moved to Hilbert_Choice.thy because their proofs need the Hilbert choice
operator. The dual of this property is also proved in theory
HOL.Hilbert_Choice.
* New syntax for the minimum/maximum of a function over a finite set:
MIN x\A. B and even MIN x. B (only useful for finite types), also MAX.
* Clarifed theorem names:
Min.antimono ~> Min.subset_imp
Max.antimono ~> Max.subset_imp
Minor INCOMPATIBILITY.
* SMT module:
- The 'smt_oracle' option is now necessary when using the 'smt' method
with a solver other than Z3. INCOMPATIBILITY.
- The encoding to first-order logic is now more complete in the
presence of higher-order quantifiers. An 'smt_explicit_application'
option has been added to control this. INCOMPATIBILITY.
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
interpretation of abstract locales. INCOMPATIBILITY.
* Predicate coprime is now a real definition, not a mere abbreviation.
INCOMPATIBILITY.
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
INCOMPATIBILITY.
* The relator rel_filter on filters has been strengthened to its
canonical categorical definition with better properties.
INCOMPATIBILITY.
* Generalized linear algebra involving linear, span, dependent, dim
from type class real_vector to locales module and vector_space.
Renamed:
span_inc ~> span_superset
span_superset ~> span_base
span_eq ~> span_eq_iff
INCOMPATIBILITY.
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.
* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every
element in a list to all following elements, not just the next one.
* Theory HOL.List syntax:
- filter-syntax "[x <- xs. P]" is no longer output syntax, but only
input syntax
- list comprehension syntax now supports tuple patterns in "pat <- xs"
* Theory Map: "empty" must now be qualified as "Map.empty".
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
clash with fact mod_mult_self4 (on more generic semirings).
INCOMPATIBILITY.
* Eliminated some theorem aliasses:
even_times_iff ~> even_mult_iff
mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
even_of_nat ~> even_int_iff
INCOMPATIBILITY.
* Eliminated some theorem duplicate variations:
- dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0
- mod_Suc_eq_Suc_mod can be replaced by mod_Suc
- mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps
- mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def
- the witness of mod_eqD can be given directly as "_ div _"
INCOMPATIBILITY.
* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no
longer aggresively destroyed to "\q. m = d * q". INCOMPATIBILITY, adding
"elim!: dvd" to classical proof methods in most situations restores
broken proofs.
* Theory HOL-Library.Conditional_Parametricity provides command
'parametric_constant' for proving parametricity of non-recursive
definitions. For constants that are not fully parametric the command
will infer conditions on relations (e.g., bi_unique, bi_total, or type
class conditions such as "respects 0") sufficient for parametricity. See
theory HOL-ex.Conditional_Parametricity_Examples for some examples.
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
generator to generate code for algebraic types with lazy evaluation
semantics even in call-by-value target languages. See the theories
HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
examples.
* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
* Theory HOL-Library.Old_Datatype no longer provides the legacy command
'old_datatype'. INCOMPATIBILITY.
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
instances of rat, real, complex as factorial rings etc. Import
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
INCOMPATIBILITY.
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new
infix/prefix notation.
* Session HOL-Algebra: revamped with much new material. The set of
isomorphisms between two groups is now denoted iso rather than iso_set.
INCOMPATIBILITY.
* Session HOL-Analysis: the Arg function now respects the same interval
as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
INCOMPATIBILITY.
* Session HOL-Analysis: the functions zorder, zer_poly, porder and
pol_poly have been redefined. All related lemmas have been reworked.
INCOMPATIBILITY.
* Session HOL-Analysis: infinite products, Moebius functions, the
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.
* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
or real-valued functions (limits, "Big-O", etc.) automatically.
See also ~~/src/HOL/Real_Asymp/Manual for some documentation.
* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
internalize_sorts and unoverload) and larger experimental application
(type based linear algebra transferred to linear algebra on subspaces).
*** ML ***
* Operation Export.export emits theory exports (arbitrary blobs), which
are stored persistently in the session build database.
* Command 'ML_export' exports ML toplevel bindings to the global
bootstrap environment of the ML process. This allows ML evaluation
without a formal theory context, e.g. in command-line tools like
"isabelle process".
*** System ***
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no
longer supported.
* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform
support has been discontinued.
* Java runtime is for x86_64 only. Corresponding Isabelle settings have
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,
instead of former 32/64 variants. INCOMPATIBILITY.
* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be
phased out due to unclear preference of 32bit vs. 64bit architecture.
Explicit GNU bash expressions are now preferred, for example (with
quotes):
#Posix executables (Unix or Cygwin), with preference for 64bit
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
#native Windows or Unix executables, with preference for 64bit
"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"
#native Windows (32bit) or Unix executables (preference for 64bit)
"${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"
* Command-line tool "isabelle build" supports new options:
- option -B NAME: include session NAME and all descendants
- option -S: only observe changes of sources, not heap images
- option -f: forces a fresh build
* Command-line tool "isabelle build" options -c -x -B refer to
descendants wrt. the session parent or import graph. Subtle
INCOMPATIBILITY: options -c -x used to refer to the session parent graph
only.
* Command-line tool "isabelle build" takes "condition" options with the
corresponding environment values into account, when determining the
up-to-date status of a session.
* The command-line tool "dump" dumps information from the cumulative
PIDE session database: many sessions may be loaded into a given logic
image, results from all loaded theories are written to the output
directory.
* Command-line tool "isabelle imports -I" also reports actual session
imports. This helps to minimize the session dependency graph.
* The command-line tool "export" and 'export_files' in session ROOT
entries retrieve theory exports from the session build database.
* The command-line tools "isabelle server" and "isabelle client" provide
access to the Isabelle Server: it supports responsive session management
and concurrent use of theories, based on Isabelle/PIDE infrastructure.
See also the "system" manual.
* The command-line tool "isabelle update_comments" normalizes formal
comments in outer syntax as follows: \ \text\ (whith a single space to
approximate the appearance in document output). This is more specific
than former "isabelle update_cartouches -c": the latter tool option has
been discontinued.
* The command-line tool "isabelle mkroot" now always produces a document
outline: its options have been adapted accordingly. INCOMPATIBILITY.
* The command-line tool "isabelle mkroot -I" initializes a Mercurial
repository for the generated session files.
* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or
ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
mode") determine the directory locations of the main build artefacts --
instead of hard-wired directories in ISABELLE_HOME_USER (or
ISABELLE_HOME).
* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
heap images and session databases are always stored in
$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or
"isabelle jedit -s" or "isabelle build -s").
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
options for improved error reporting. Potential INCOMPATIBILITY with
unusual LaTeX installations, may have to adapt these settings.
* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE
markup for identifier bindings. It now uses The GNU Multiple Precision
Arithmetic Library (libgmp) on all platforms, notably Mac OS X with
32/64 bit.
New in Isabelle2017 (October 2017)
----------------------------------
*** General ***
* Experimental support for Visual Studio Code (VSCode) as alternative
Isabelle/PIDE front-end, see also
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017
VSCode is a new type of application that continues the concepts of
"programmer's editor" and "integrated development environment" towards
fully semantic editing and debugging -- in a relatively light-weight
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
Technically, VSCode is based on the Electron application framework
(Node.js + Chromium browser + V8), which is implemented in JavaScript
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
modules around a Language Server implementation.
* Theory names are qualified by the session name that they belong to.
This affects imports, but not the theory name space prefix (which is
just the theory base name as before).
In order to import theories from other sessions, the ROOT file format
provides a new 'sessions' keyword. In contrast, a theory that is
imported in the old-fashioned manner via an explicit file-system path
belongs to the current session, and might cause theory name conflicts
later on. Theories that are imported from other sessions are excluded
from the current session document. The command-line tool "isabelle
imports" helps to update theory imports.
* The main theory entry points for some non-HOL sessions have changed,
to avoid confusion with the global name "Main" of the session HOL. This
leads to the follow renamings:
CTT/Main.thy ~> CTT/CTT.thy
ZF/Main.thy ~> ZF/ZF.thy
ZF/Main_ZF.thy ~> ZF/ZF.thy
ZF/Main_ZFC.thy ~> ZF/ZFC.thy
ZF/ZF.thy ~> ZF/ZF_Base.thy
INCOMPATIBILITY.
* Commands 'alias' and 'type_alias' introduce aliases for constants and
type constructors, respectively. This allows adhoc changes to name-space
accesses within global or local theory contexts, e.g. within a 'bundle'.
* Document antiquotations @{prf} and @{full_prf} output proof terms
(again) in the same way as commands 'prf' and 'full_prf'.
* Computations generated by the code generator can be embedded directly
into ML, alongside with @{code} antiquotations, using the following
antiquotations:
@{computation ... terms: ... datatypes: ...} :
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
@{computation_conv ... terms: ... datatypes: ...} :
(Proof.context -> 'ml -> conv) -> Proof.context -> conv
@{computation_check terms: ... datatypes: ...} : Proof.context -> conv
See src/HOL/ex/Computations.thy,
src/HOL/Decision_Procs/Commutative_Ring.thy and
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Session-qualified theory imports allow the Prover IDE to process
arbitrary theory hierarchies independently of the underlying logic
session image (e.g. option "isabelle jedit -l"), but the directory
structure needs to be known in advance (e.g. option "isabelle jedit -d"
or a line in the file $ISABELLE_HOME_USER/ROOTS).
* The PIDE document model maintains file content independently of the
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
changes of formal document content. Theory dependencies are always
resolved internally, without the need for corresponding editor buffers.
The system option "jedit_auto_load" has been discontinued: it is
effectively always enabled.
* The Theories dockable provides a "Purge" button, in order to restrict
the document model to theories that are required for open editor
buffers.
* The Theories dockable indicates the overall status of checking of each
entry. When all forked tasks of a theory are finished, the border is
painted with thick lines; remaining errors in this situation are
represented by a different border color.
* Automatic indentation is more careful to avoid redundant spaces in
intermediate situations. Keywords are indented after input (via typed
characters or completion); see also option "jedit_indent_input".
* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.
* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
entry of the specified logic session in the editor, while its parent is
used for formal checking.
* The main Isabelle/jEdit plugin may be restarted manually (using the
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
enabled at all times.
* Update to current jedit-5.4.0.
*** Pure ***
* Deleting the last code equations for a particular function using
[code del] results in function with no equations (runtime abort) rather
than an unimplemented function (generation time abort). Use explicit
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
* Proper concept of code declarations in code.ML:
- Regular code declarations act only on the global theory level, being
ignored with warnings if syntactically malformed.
- Explicitly global code declarations yield errors if syntactically
malformed.
- Default code declarations are silently ignored if syntactically
malformed.
Minor INCOMPATIBILITY.
* Clarified and standardized internal data bookkeeping of code
declarations: history of serials allows to track potentially
non-monotonous declarations appropriately. Minor INCOMPATIBILITY.
*** HOL ***
* The Nunchaku model finder is now part of "Main".
* SMT module:
- A new option, 'smt_nat_as_int', has been added to translate 'nat' to
'int' and benefit from the SMT solver's theory reasoning. It is
disabled by default.
- The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.
- Several small issues have been rectified in the 'smt' command.
* (Co)datatype package: The 'size_gen_o_map' lemma is no longer
generated for datatypes with type class annotations. As a result, the
tactic that derives it no longer fails on nested datatypes. Slight
INCOMPATIBILITY.
* Command and antiquotation "value" with modified default strategy:
terms without free variables are always evaluated using plain evaluation
only, with no fallback on normalization by evaluation. Minor
INCOMPATIBILITY.
* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").
* Constant "surj" is a full input/output abbreviation (again).
Minor INCOMPATIBILITY.
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
INCOMPATIBILITY.
* Renamed ii to imaginary_unit in order to free up ii as a variable
name. The syntax \ remains available. INCOMPATIBILITY.
* Dropped abbreviations transP, antisymP, single_valuedP; use constants
transp, antisymp, single_valuedp instead. INCOMPATIBILITY.
* Constant "subseq" in Topological_Spaces has been removed -- it is
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
* Theory List: "sublist" renamed to "nths" in analogy with "nth", and
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
* Theory List: new generic function "sorted_wrt".
* Named theorems mod_simps covers various congruence rules concerning
mod, replacing former zmod_simps. INCOMPATIBILITY.
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
mod_diff_eq. INCOMPATIBILITY.
* Generalized some facts:
measure_induct_rule
measure_induct
zminus_zmod ~> mod_minus_eq
zdiff_zmod_left ~> mod_diff_left_eq
zdiff_zmod_right ~> mod_diff_right_eq
zmod_eq_dvd_iff ~> mod_eq_dvd_iff
INCOMPATIBILITY.
* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
euclidean_(semi)ring, euclidean_(semi)ring_cancel,
unique_euclidean_(semi)ring; instantiation requires provision of a
euclidean size.
* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:
- Euclidean induction is available as rule eucl_induct.
- Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
easy instantiation of euclidean (semi)rings as GCD (semi)rings.
- Coefficients obtained by extended euclidean algorithm are
available as "bezout_coefficients".
INCOMPATIBILITY.
* Theory "Number_Theory.Totient" introduces basic notions about Euler's
totient function previously hidden as solitary example in theory
Residues. Definition changed so that "totient 1 = 1" in agreement with
the literature. Minor INCOMPATIBILITY.
* New styles in theory "HOL-Library.LaTeXsugar":
- "dummy_pats" for printing equations with "_" on the lhs;
- "eta_expand" for printing eta-expanded terms.
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
filter for describing points x such that f(x) is in the filter F.
* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
space. INCOMPATIBILITY.
* Theory "HOL-Library.FinFun" has been moved to AFP (again).
INCOMPATIBILITY.
* Theory "HOL-Library.FuncSet": some old and rarely used ASCII
replacement syntax has been removed. INCOMPATIBILITY, standard syntax
with symbols should be used instead. The subsequent commands help to
reproduce the old forms, e.g. to simplify porting old theories:
syntax (ASCII)
"_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PIE _:_./ _)" 10)
"_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PI _:_./ _)" 10)
"_lam" :: "pttrn \ 'a set \ 'a \ 'b \ ('a \ 'b)" ("(3%_:_./ _)" [0,0,3] 3)
* Theory "HOL-Library.Multiset": the simprocs on subsets operators of
multisets have been renamed:
msetless_cancel_numerals ~> msetsubset_cancel
msetle_cancel_numerals ~> msetsubset_eq_cancel
INCOMPATIBILITY.
* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
for pattern aliases as known from Haskell, Scala and ML.
* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
* Session HOL-Analysis: more material involving arcs, paths, covering
spaces, innessential maps, retracts, infinite products, simplicial
complexes. Baire Category theorem. Major results include the Jordan
Curve Theorem and the Great Picard Theorem.
* Session HOL-Algebra has been extended by additional lattice theory:
the Knaster-Tarski fixed point theorem and Galois Connections.
* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions
of squarefreeness, n-th powers, and prime powers.
* Session "HOL-Computional_Algebra" covers many previously scattered
theories, notably Euclidean_Algorithm, Factorial_Ring,
Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,
Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor
INCOMPATIBILITY.
*** System ***
* Isabelle/Scala: the SQL module supports access to relational
databases, either as plain file (SQLite) or full-scale server
(PostgreSQL via local port or remote ssh connection).
* Results of "isabelle build" are recorded as SQLite database (i.e.
"Application File Format" in the sense of
https://www.sqlite.org/appfileformat.html). This allows systematic
access via operations from module Sessions.Store in Isabelle/Scala.
* System option "parallel_proofs" is 1 by default (instead of more
aggressive 2). This requires less heap space and avoids burning parallel
CPU cycles, while full subproof parallelization is enabled for repeated
builds (according to parallel_subproofs_threshold).
* System option "record_proofs" allows to change the global
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
a negative value means the current state in the ML heap image remains
unchanged.
* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been
renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.
* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the
native Windows platform (independently of the Cygwin installation). This
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
ISABELLE_PLATFORM64.
* Command-line tool "isabelle build_docker" builds a Docker image from
the Isabelle application bundle for Linux. See also
https://hub.docker.com/r/makarius/isabelle
* Command-line tool "isabelle vscode_server" provides a Language Server
Protocol implementation, e.g. for the Visual Studio Code editor. It
serves as example for alternative PIDE front-ends.
* Command-line tool "isabelle imports" helps to maintain theory imports
wrt. session structure. Examples for the main Isabelle distribution:
isabelle imports -I -a
isabelle imports -U -a
isabelle imports -U -i -a
isabelle imports -M -a -d '~~/src/Benchmarks'
New in Isabelle2016-1 (December 2016)
-------------------------------------
*** General ***
* Splitter in proof methods "simp", "auto" and friends:
- The syntax "split add" has been discontinued, use plain "split",
INCOMPATIBILITY.
- For situations with many conditional or case expressions, there is
an alternative splitting strategy that can be much faster. It is
selected by writing "split!" instead of "split". It applies safe
introduction and elimination rules after each split rule. As a
result the subgoal may be split into several subgoals.
* Command 'bundle' provides a local theory target to define a bundle
from the body of specification commands (such as 'declare',
'declaration', 'notation', 'lemmas', 'lemma'). For example:
bundle foo
begin
declare a [simp]
declare b [intro]
end
* Command 'unbundle' is like 'include', but works within a local theory
context. Unlike "context includes ... begin", the effect of 'unbundle'
on the target context persists, until different declarations are given.
* Simplified outer syntax: uniform category "name" includes long
identifiers. Former "xname" / "nameref" / "name reference" has been
discontinued.
* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.
* Mixfix annotations support general block properties, with syntax
"(\x=a y=b z \\". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
to "(\indent=DIGITS\". The former notation "(00" for unbreakable blocks
is superseded by "(\unbreabable\" --- rare INCOMPATIBILITY.
* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.
* Commands 'prf' and 'full_prf' are somewhat more informative (again):
proof terms are reconstructed and cleaned from administrative thm nodes.
* Code generator: config option "code_timing" triggers measurements of
different phases of code generation. See src/HOL/ex/Code_Timing.thy for
examples.
* Code generator: implicits in Scala (stemming from type class
instances) are generated into companion object of corresponding type
class, to resolve some situations where ambiguities may occur.
* Solve direct: option "solve_direct_strict_warnings" gives explicit
warnings for lemma statements with trivial proofs.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* More aggressive flushing of machine-generated input, according to
system option editor_generated_input_delay (in addition to existing
editor_input_delay for regular user edits). This may affect overall PIDE
reactivity and CPU usage.
* Syntactic indentation according to Isabelle outer syntax. Action
"indent-lines" (shortcut C+i) indents the current line according to
command keywords and some command substructure. Action
"isabelle.newline" (shortcut ENTER) indents the old and the new line
according to command keywords only; see also option
"jedit_indent_newline".
* Semantic indentation for unstructured proof scripts ('apply' etc.) via
number of subgoals. This requires information of ongoing document
processing and may thus lag behind, when the user is editing too
quickly; see also option "jedit_script_indent" and
"jedit_script_indent_limit".
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure; 'begin' and 'end'
structure of theory specifications is treated as well.
* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".
* Completion templates for commands involving "begin ... end" blocks,
e.g. 'context', 'notepad'.
* Sidekick parser "isabelle-context" shows nesting of context blocks
according to 'begin' and 'end' structure.
* Highlighting of entity def/ref positions wrt. cursor.
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
occurrences of the formal entity at the caret position. This facilitates
systematic renaming.
* PIDE document markup works across multiple Isar commands, e.g. the
results established at the end of a proof are properly identified in the
theorem statement.
* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.
* Dockable window "Symbols" also provides access to 'abbrevs' from the
outer syntax of the current theory buffer. This provides clickable
syntax templates, including entries with empty abbrevs name (which are
inaccessible via keyboard completion).
* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:
src/Pure/ROOT0.ML
src/Pure/ROOT.ML
src/Pure/Pure.thy
src/Pure/ML_Bootstrap.thy
The ML ROOT files act like quasi-theories in the context of theory
ML_Bootstrap: this allows continuous checking of all loaded ML files.
The theory files are presented with a modified header to import Pure
from the running Isabelle instance. Results from changed versions of
each stage are *not* propagated to the next stage, and isolated from the
actual Isabelle/Pure that runs the IDE itself. The sequential
dependencies of the above files are only observed for batch build.
* Isabelle/ML and Standard ML files are presented in Sidekick with the
tree structure of section headings: this special comment format is
described in "implementation" chapter 0, e.g. (*** section ***).
* Additional abbreviations for syntactic completion may be specified
within the theory header as 'abbrevs'. The theory syntax for 'keywords'
has been simplified accordingly: optional abbrevs need to go into the
new 'abbrevs' section.
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
INCOMPATIBILITY, use 'abbrevs' within theory header instead.
* Action "isabelle.keymap-merge" asks the user to resolve pending
Isabelle keymap changes that are in conflict with the current jEdit
keymap; non-conflicting changes are always applied implicitly. This
action is automatically invoked on Isabelle/jEdit startup and thus
increases chances that users see new keyboard shortcuts when re-using
old keymaps.
* ML and document antiquotations for file-systems paths are more uniform
and diverse:
@{path NAME} -- no file-system check
@{file NAME} -- check for plain file
@{dir NAME} -- check for directory
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
have to be changed.
*** Document preparation ***
* New symbol \, e.g. for temporal operator.
* New document and ML antiquotation @{locale} for locales, similar to
existing antiquotation @{class}.
* Mixfix annotations support delimiters like \<^control>\cartouche\ --
this allows special forms of document output.
* Raw LaTeX output now works via \<^latex>\...\ instead of raw control
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
derivatives.
* \<^raw:...> symbols are no longer supported.
* Old 'header' command is no longer supported (legacy since
Isabelle2015).
*** Isar ***
* Many specification elements support structured statements with 'if' /
'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
'definition', 'inductive', 'function'.
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
"that" or "assms", respectively. Empty premises are *not* bound in the
context: INCOMPATIBILITY.
* Command 'define' introduces a local (non-polymorphic) definition, with
optional abstraction over local parameters. The syntax resembles
'definition' and 'obtain'. It fits better into the Isar language than
old 'def', which is now a legacy feature.
* Command 'obtain' supports structured statements with 'if' / 'for'
context.
* Command '\' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.
* The defining position of a literal fact \prop\ is maintained more
carefully, and made accessible as hyperlink in the Prover IDE.
* Commands 'finally' and 'ultimately' used to expose the result as
literal fact: this accidental behaviour has been discontinued. Rare
INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
* Command 'axiomatization' has become more restrictive to correspond
better to internal axioms as singleton facts with mandatory name. Minor
INCOMPATIBILITY.
* Proof methods may refer to the main facts via the dynamic fact
"method_facts". This is particularly useful for Eisbach method
definitions.
* Proof method "use" allows to modify the main facts of a given method
expression, e.g.
(use facts in simp)
(use facts in \simp add: ...\)
* The old proof method "default" has been removed (legacy since
Isabelle2016). INCOMPATIBILITY, use "standard" instead.
*** Pure ***
* Pure provides basic versions of proof methods "simp" and "simp_all"
that only know about meta-equality (==). Potential INCOMPATIBILITY in
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
is relevant to avoid confusion of Pure.simp vs. HOL.simp.
* The command 'unfolding' and proof method "unfold" include a second
stage where given equations are passed through the attribute "abs_def"
before rewriting. This ensures that definitions are fully expanded,
regardless of the actual parameters that are provided. Rare
INCOMPATIBILITY in some corner cases: use proof method (simp only:)
instead, or declare [[unfold_abs_def = false]] in the proof context.
* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "\x. P x" without any further syntactic context
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
INCOMPATIBILITY, need to provide explicit type constraints for Pure
types where this is really intended.
*** HOL ***
* New proof method "argo" using the built-in Argo solver based on SMT
technology. The method can be used to prove goals of quantifier-free
propositional logic, goals based on a combination of quantifier-free
propositional logic with equality, and goals based on a combination of
quantifier-free propositional logic with linear real arithmetic
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
* The new "nunchaku" command integrates the Nunchaku model finder. The
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
* Metis: The problem encoding has changed very slightly. This might
break existing proofs. INCOMPATIBILITY.
* Sledgehammer:
- The MaSh relevance filter is now faster than before.
- Produce syntactically correct Vampire 4.0 problem files.
* (Co)datatype package:
- New commands for defining corecursive functions and reasoning about
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
method. See 'isabelle doc corec'.
- The predicator :: ('a \ bool) \ 'a F \ bool is now a first-class
citizen in bounded natural functors.
- 'primrec' now allows nested calls through the predicator in addition
to the map function.
- 'bnf' automatically discharges reflexive proof obligations.
- 'bnf' outputs a slightly modified proof obligation expressing rel in
terms of map and set
(not giving a specification for rel makes this one reflexive).
- 'bnf' outputs a new proof obligation expressing pred in terms of set
(not giving a specification for pred makes this one reflexive).
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment.
- Renamed lemmas:
rel_prod_apply ~> rel_prod_inject
pred_prod_apply ~> pred_prod_inject
INCOMPATIBILITY.
- The "size" plugin has been made compatible again with locales.
- The theorems about "rel" and "set" may have a slightly different (but
equivalent) form.
INCOMPATIBILITY.
* The 'coinductive' command produces a proper coinduction rule for
mutual coinductive predicates. This new rule replaces the old rule,
which exposed details of the internal fixpoint construction and was
hard to use. INCOMPATIBILITY.
* New abbreviations for negated existence (but not bounded existence):
\x. P x \ \ (\x. P x)
\!x. P x \ \ (\!x. P x)
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
has been removed for output. It is retained for input only, until it is
eliminated altogether.
* The unique existence quantifier no longer provides 'binder' syntax,
but uses syntax translations (as for bounded unique existence). Thus
iterated quantification \!x y. P x y with its slightly confusing
sequential meaning \!x. \!y. P x y is no longer possible. Instead,
pattern abstraction admits simultaneous unique existence \!(x, y). P x y
(analogous to existing notation \!(x, y)\A. P x y). Potential
INCOMPATIBILITY in rare situations.
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
INCOMPATIBILITY.
* Renamed constants and corresponding theorems:
setsum ~> sum
setprod ~> prod
listsum ~> sum_list
listprod ~> prod_list
INCOMPATIBILITY.
* Sligthly more standardized theorem names:
sgn_times ~> sgn_mult
sgn_mult' ~> Real_Vector_Spaces.sgn_mult
divide_zero_left ~> div_0
zero_mod_left ~> mod_0
divide_zero ~> div_by_0
divide_1 ~> div_by_1
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
mod_div_equality ~> div_mult_mod_eq
mod_div_equality2 ~> mult_div_mod_eq
mod_div_equality3 ~> mod_div_mult_eq
mod_div_equality4 ~> mod_mult_div_eq
minus_div_eq_mod ~> minus_div_mult_eq_mod
minus_div_eq_mod2 ~> minus_mult_div_eq_mod
minus_mod_eq_div ~> minus_mod_eq_div_mult
minus_mod_eq_div2 ~> minus_mod_eq_mult_div
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
div_1 ~> div_by_Suc_0
mod_1 ~> mod_by_Suc_0
INCOMPATIBILITY.
* New type class "idom_abs_sgn" specifies algebraic properties
of sign and absolute value functions. Type class "sgn_if" has
disappeared. Slight INCOMPATIBILITY.
* Dedicated syntax LENGTH('a) for length of types.
* Characters (type char) are modelled as finite algebraic type
corresponding to {0..255}.
- Logical representation:
* 0 is instantiated to the ASCII zero character.
* All other characters are represented as "Char n"
with n being a raw numeral expression less than 256.
* Expressions of the form "Char n" with n greater than 255
are non-canonical.
- Printing and parsing:
* Printable characters are printed and parsed as "CHR ''\''"
(as before).
* The ASCII zero character is printed and parsed as "0".
* All other canonical characters are printed as "CHR 0xXX"
with XX being the hexadecimal character code. "CHR n"
is parsable for every numeral expression n.
* Non-canonical characters have no special syntax and are
printed as their logical representation.
- Explicit conversions from and to the natural numbers are
provided as char_of_nat, nat_of_char (as before).
- The auxiliary nibble type has been discontinued.
INCOMPATIBILITY.
* Type class "div" with operation "mod" renamed to type class "modulo"
with operation "modulo", analogously to type class "divide". This
eliminates the need to qualify any of those names in the presence of
infix "mod" syntax. INCOMPATIBILITY.
* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
have been clarified. The fixpoint properties are lfp_fixpoint, its
symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
for the proof (lfp_lemma2 etc.) are no longer exported, but can be
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
* Constant "surj" is a mere input abbreviation, to avoid hiding an
equation in term output. Minor INCOMPATIBILITY.
* Command 'code_reflect' accepts empty constructor lists for datatypes,
which renders those abstract effectively.
* Command 'export_code' checks given constants for abstraction
violations: a small guarantee that given constants specify a safe
interface for the generated code.
* Code generation for Scala: ambiguous implicts in class diagrams are
spelt out explicitly.
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
explicitly provided auxiliary definitions for required type class
dictionaries rather than half-working magic. INCOMPATIBILITY, see the
tutorial on code generation for details.
* Theory Set_Interval: substantial new theorems on indexed sums and
products.
* Locale bijection establishes convenient default simp rules such as
"inv f (f a) = a" for total bijections.
* Abstract locales semigroup, abel_semigroup, semilattice,
semilattice_neutr, ordering, ordering_top, semilattice_order,
semilattice_neutr_order, comm_monoid_set, semilattice_set,
semilattice_neutr_set, semilattice_order_set,
semilattice_order_neutr_set monoid_list, comm_monoid_list,
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified
syntax uniformly that does not clash with corresponding global syntax.
INCOMPATIBILITY.
* Former locale lifting_syntax is now a bundle, which is easier to
include in a local context or theorem statement, e.g. "context includes
lifting_syntax begin ... end". Minor INCOMPATIBILITY.
* Some old / obsolete theorems have been renamed / removed, potential
INCOMPATIBILITY.
nat_less_cases -- removed, use linorder_cases instead
inv_image_comp -- removed, use image_inv_f_f instead
image_surj_f_inv_f ~> image_f_inv_f
* Some theorems about groups and orders have been generalised from
groups to semi-groups that are also monoids:
le_add_same_cancel1
le_add_same_cancel2
less_add_same_cancel1
less_add_same_cancel2
add_le_same_cancel1
add_le_same_cancel2
add_less_same_cancel1
add_less_same_cancel2
* Some simplifications theorems about rings have been removed, since
superseeded by a more general version:
less_add_cancel_left_greater_zero ~> less_add_same_cancel1
less_add_cancel_right_greater_zero ~> less_add_same_cancel2
less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
less_add_cancel_left_less_zero ~> add_less_same_cancel1
less_add_cancel_right_less_zero ~> add_less_same_cancel2
INCOMPATIBILITY.
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
resemble the f.split naming convention, INCOMPATIBILITY.
* Added class topological_monoid.
* The following theorems have been renamed:
setsum_left_distrib ~> sum_distrib_right
setsum_right_distrib ~> sum_distrib_left
INCOMPATIBILITY.
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
INCOMPATIBILITY.
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f `
A)".
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.
* The type class ordered_comm_monoid_add is now called
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add
is introduced as the combination of ordered_ab_semigroup_add +
comm_monoid_add. INCOMPATIBILITY.
* Introduced the type classes canonically_ordered_comm_monoid_add and
dioid.
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
instantiating linordered_semiring_strict and ordered_ab_group_add, an
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might
be required. INCOMPATIBILITY.
* Dropped various legacy fact bindings, whose replacements are often
of a more general type also:
lcm_left_commute_nat ~> lcm.left_commute
lcm_left_commute_int ~> lcm.left_commute
gcd_left_commute_nat ~> gcd.left_commute
gcd_left_commute_int ~> gcd.left_commute
gcd_greatest_iff_nat ~> gcd_greatest_iff
gcd_greatest_iff_int ~> gcd_greatest_iff
coprime_dvd_mult_nat ~> coprime_dvd_mult
coprime_dvd_mult_int ~> coprime_dvd_mult
zpower_numeral_even ~> power_numeral_even
gcd_mult_cancel_nat ~> gcd_mult_cancel
gcd_mult_cancel_int ~> gcd_mult_cancel
div_gcd_coprime_nat ~> div_gcd_coprime
div_gcd_coprime_int ~> div_gcd_coprime
zpower_numeral_odd ~> power_numeral_odd
zero_less_int_conv ~> of_nat_0_less_iff
gcd_greatest_nat ~> gcd_greatest
gcd_greatest_int ~> gcd_greatest
coprime_mult_nat ~> coprime_mult
coprime_mult_int ~> coprime_mult
lcm_commute_nat ~> lcm.commute
lcm_commute_int ~> lcm.commute
int_less_0_conv ~> of_nat_less_0_iff
gcd_commute_nat ~> gcd.commute
gcd_commute_int ~> gcd.commute
Gcd_insert_nat ~> Gcd_insert
Gcd_insert_int ~> Gcd_insert
of_int_int_eq ~> of_int_of_nat_eq
lcm_least_nat ~> lcm_least
lcm_least_int ~> lcm_least
lcm_assoc_nat ~> lcm.assoc
lcm_assoc_int ~> lcm.assoc
int_le_0_conv ~> of_nat_le_0_iff
int_eq_0_conv ~> of_nat_eq_0_iff
Gcd_empty_nat ~> Gcd_empty
Gcd_empty_int ~> Gcd_empty
gcd_assoc_nat ~> gcd.assoc
gcd_assoc_int ~> gcd.assoc
zero_zle_int ~> of_nat_0_le_iff
lcm_dvd2_nat ~> dvd_lcm2
lcm_dvd2_int ~> dvd_lcm2
lcm_dvd1_nat ~> dvd_lcm1
lcm_dvd1_int ~> dvd_lcm1
gcd_zero_nat ~> gcd_eq_0_iff
gcd_zero_int ~> gcd_eq_0_iff
gcd_dvd2_nat ~> gcd_dvd2
gcd_dvd2_int ~> gcd_dvd2
gcd_dvd1_nat ~> gcd_dvd1
gcd_dvd1_int ~> gcd_dvd1
int_numeral ~> of_nat_numeral
lcm_ac_nat ~> ac_simps
lcm_ac_int ~> ac_simps
gcd_ac_nat ~> ac_simps
gcd_ac_int ~> ac_simps
abs_int_eq ~> abs_of_nat
zless_int ~> of_nat_less_iff
zdiff_int ~> of_nat_diff
zadd_int ~> of_nat_add
int_mult ~> of_nat_mult
int_Suc ~> of_nat_Suc
inj_int ~> inj_of_nat
int_1 ~> of_nat_1
int_0 ~> of_nat_0
Lcm_empty_nat ~> Lcm_empty
Lcm_empty_int ~> Lcm_empty
Lcm_insert_nat ~> Lcm_insert
Lcm_insert_int ~> Lcm_insert
comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
Lcm_eq_0 ~> Lcm_eq_0_I
Lcm0_iff ~> Lcm_0_iff
Lcm_dvd_int ~> Lcm_least
divides_mult_nat ~> divides_mult
divides_mult_int ~> divides_mult
lcm_0_nat ~> lcm_0_right
lcm_0_int ~> lcm_0_right
lcm_0_left_nat ~> lcm_0_left
lcm_0_left_int ~> lcm_0_left
dvd_gcd_D1_nat ~> dvd_gcdD1
dvd_gcd_D1_int ~> dvd_gcdD1
dvd_gcd_D2_nat ~> dvd_gcdD2
dvd_gcd_D2_int ~> dvd_gcdD2
coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
realpow_minus_mult ~> power_minus_mult
realpow_Suc_le_self ~> power_Suc_le_self
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
INCOMPATIBILITY.
* Renamed HOL/Quotient_Examples/FSet.thy to
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
* Session HOL-Library: theory FinFun bundles "finfun_syntax" and
"no_finfun_syntax" allow to control optional syntax in local contexts;
this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use
"unbundle finfun_syntax" to imitate import of
"~~/src/HOL/Library/FinFun_Syntax".
* Session HOL-Library: theory Multiset_Permutations (executably) defines
the set of permutations of a given set or multiset, i.e. the set of all
lists that contain every element of the carrier (multi-)set exactly
once.
* Session HOL-Library: multiset membership is now expressed using
set_mset rather than count.
- Expressions "count M a > 0" and similar simplify to membership
by default.
- Converting between "count M a = 0" and non-membership happens using
equations count_eq_zero_iff and not_in_iff.
- Rules count_inI and in_countE obtain facts of the form
"count M a = n" from membership.
- Rules count_in_diffI and in_diff_countE obtain facts of the form
"count M a = n + count N a" from membership on difference sets.
INCOMPATIBILITY.
* Session HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for
displaying equations in functional programming style --- variables
present on the left-hand but not on the righ-hand side are replaced by
underscores.
* Session HOL-Library: theory Combinator_PER provides combinator to
build partial equivalence relations from a predicate and an equivalence
relation.
* Session HOL-Library: theory Perm provides basic facts about almost
everywhere fix bijections.
* Session HOL-Library: theory Normalized_Fraction allows viewing an
element of a field of fractions as a normalized fraction (i.e. a pair of
numerator and denominator such that the two are coprime and the
denominator is normalized wrt. unit factors).
* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
* Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis.
* Session HOL-Analysis: measure theory has been moved here from
HOL-Probability. When importing HOL-Analysis some theorems need
additional name spaces prefixes due to name clashes. INCOMPATIBILITY.
* Session HOL-Analysis: more complex analysis including Cauchy's
inequality, Liouville theorem, open mapping theorem, maximum modulus
principle, Residue theorem, Schwarz Lemma.
* Session HOL-Analysis: Theory of polyhedra: faces, extreme points,
polytopes, and the Krein–Milman Minkowski theorem.
* Session HOL-Analysis: Numerous results ported from the HOL Light
libraries: homeomorphisms, continuous function extensions, invariance of
domain.
* Session HOL-Probability: the type of emeasure and nn_integral was
changed from ereal to ennreal, INCOMPATIBILITY.
emeasure :: 'a measure \ 'a set \ ennreal
nn_integral :: 'a measure \ ('a \ ennreal) \ ennreal
* Session HOL-Probability: Code generation and QuickCheck for
Probability Mass Functions.
* Session HOL-Probability: theory Random_Permutations contains some
theory about choosing a permutation of a set uniformly at random and
folding over a list in random order.
* Session HOL-Probability: theory SPMF formalises discrete
subprobability distributions.
* Session HOL-Library: the names of multiset theorems have been
normalised to distinguish which ordering the theorems are about
mset_less_eqI ~> mset_subset_eqI
mset_less_insertD ~> mset_subset_insertD
mset_less_eq_count ~> mset_subset_eq_count
mset_less_diff_self ~> mset_subset_diff_self
mset_le_exists_conv ~> mset_subset_eq_exists_conv
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
mset_le_mono_add ~> mset_subset_eq_mono_add
mset_le_add_left ~> mset_subset_eq_add_left
mset_le_add_right ~> mset_subset_eq_add_right
mset_le_single ~> mset_subset_eq_single
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
diff_le_self ~> diff_subset_eq_self
mset_leD ~> mset_subset_eqD
mset_lessD ~> mset_subsetD
mset_le_insertD ~> mset_subset_eq_insertD
mset_less_of_empty ~> mset_subset_of_empty
mset_less_size ~> mset_subset_size
wf_less_mset_rel ~> wf_subset_mset_rel
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
mset_remdups_le ~> mset_remdups_subset_eq
ms_lesseq_impl ~> subset_eq_mset_impl
Some functions have been renamed:
ms_lesseq_impl -> subset_eq_mset_impl
* HOL-Library: multisets are now ordered with the multiset ordering
#\# ~> \
#\# ~> <
le_multiset ~> less_eq_multiset
less_multiset ~> le_multiset
INCOMPATIBILITY.
* Session HOL-Library: the prefix multiset_order has been discontinued:
the theorems can be directly accessed. As a consequence, the lemmas
"order_multiset" and "linorder_multiset" have been discontinued, and the
interpretations "multiset_linorder" and "multiset_wellorder" have been
replaced by instantiations. INCOMPATIBILITY.
* Session HOL-Library: some theorems about the multiset ordering have
been renamed:
le_multiset_def ~> less_eq_multiset_def
less_multiset_def ~> le_multiset_def
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
mult_less_not_refl ~> mset_le_not_refl
mult_less_trans ~> mset_le_trans
mult_less_not_sym ~> mset_le_not_sym
mult_less_asym ~> mset_le_asym
mult_less_irrefl ~> mset_le_irrefl
union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
le_multiset_total ~> less_eq_multiset_total
less_multiset_right_total ~> subset_eq_imp_le_multiset
le_multiset_empty_left ~> less_eq_multiset_empty_left
le_multiset_empty_right ~> less_eq_multiset_empty_right
less_multiset_empty_right ~> le_multiset_empty_left
less_multiset_empty_left ~> le_multiset_empty_right
union_less_diff_plus ~> union_le_diff_plus
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
INCOMPATIBILITY.
* Session HOL-Library: the lemma mset_map has now the attribute [simp].
INCOMPATIBILITY.
* Session HOL-Library: some theorems about multisets have been removed.
INCOMPATIBILITY, use the following replacements:
le_multiset_plus_plus_left_iff ~> add_less_cancel_right
less_multiset_plus_plus_left_iff ~> add_less_cancel_right
le_multiset_plus_plus_right_iff ~> add_less_cancel_left
less_multiset_plus_plus_right_iff ~> add_less_cancel_left
add_eq_self_empty_iff ~> add_cancel_left_right
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right
empty_inter ~> subset_mset.inf_bot_left
inter_empty ~> subset_mset.inf_bot_right
empty_sup ~> subset_mset.sup_bot_left
sup_empty ~> subset_mset.sup_bot_right
bdd_below_multiset ~> subset_mset.bdd_above_bot
subset_eq_empty ~> subset_mset.le_zero_eq
le_empty ~> subset_mset.le_zero_eq
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
* Session HOL-Library: some typeclass constraints about multisets have
been reduced from ordered or linordered to preorder. Multisets have the
additional typeclasses order_bot, no_top,
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
linordered_cancel_ab_semigroup_add, and
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY.
* Session HOL-Library: there are some new simplification rules about
multisets, the multiset ordering, and the subset ordering on multisets.
INCOMPATIBILITY.
* Session HOL-Library: the subset ordering on multisets has now the
interpretations ordered_ab_semigroup_monoid_add_imp_le and
bounded_lattice_bot. INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: single has been removed in favor
of add_mset that roughly corresponds to Set.insert. Some theorems have
removed or changed:
single_not_empty ~> add_mset_not_empty or empty_not_add_mset
fold_mset_insert ~> fold_mset_add_mset
image_mset_insert ~> image_mset_add_mset
union_single_eq_diff
multi_self_add_other_not_self
diff_single_eq_union
INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: some theorems have been changed
to use add_mset instead of single:
mset_add
multi_self_add_other_not_self
diff_single_eq_union
union_single_eq_diff
union_single_eq_member
add_eq_conv_diff
insert_noteq_member
add_eq_conv_ex
multi_member_split
multiset_add_sub_el_shuffle
mset_subset_eq_insertD
mset_subset_insertD
insert_subset_eq_iff
insert_union_subset_iff
multi_psub_of_add_self
inter_add_left1
inter_add_left2
inter_add_right1
inter_add_right2
sup_union_left1
sup_union_left2
sup_union_right1
sup_union_right2
size_eq_Suc_imp_eq_union
multi_nonempty_split
mset_insort
mset_update
mult1I
less_add
mset_zip_take_Cons_drop_twice
rel_mset_Zero
msed_map_invL
msed_map_invR
msed_rel_invL
msed_rel_invR
le_multiset_right_total
multiset_induct
multiset_induct2_size
multiset_induct2
INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: the definitions of some
constants have changed to use add_mset instead of adding a single
element:
image_mset
mset
replicate_mset
mult1
pred_mset
rel_mset'
mset_insort
INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: due to the above changes, the
attributes of some multiset theorems have been changed:
insert_DiffM [] ~> [simp]
insert_DiffM2 [simp] ~> []
diff_add_mset_swap [simp]
fold_mset_add_mset [simp]
diff_diff_add [simp] (for multisets only)
diff_cancel [simp] ~> []
count_single [simp] ~> []
set_mset_single [simp] ~> []
size_multiset_single [simp] ~> []
size_single [simp] ~> []
image_mset_single [simp] ~> []
mset_subset_eq_mono_add_right_cancel [simp] ~> []
mset_subset_eq_mono_add_left_cancel [simp] ~> []
fold_mset_single [simp] ~> []
subset_eq_empty [simp] ~> []
empty_sup [simp] ~> []
sup_empty [simp] ~> []
inter_empty [simp] ~> []
empty_inter [simp] ~> []
INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: the order of the variables in
the second cases of multiset_induct, multiset_induct2_size,
multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: there is now a simplification
procedure on multisets. It mimics the behavior of the procedure on
natural numbers. INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: renamed sums and products of
multisets:
msetsum ~> sum_mset
msetprod ~> prod_mset
* Session HOL-Library, theory Multiset: the notation for intersection
and union of multisets have been changed:
#\ ~> \#
#\ ~> \#
INCOMPATIBILITY.
* Session HOL-Library, theory Multiset: the lemma
one_step_implies_mult_aux on multisets has been removed, use
one_step_implies_mult instead. INCOMPATIBILITY.
* Session HOL-Library: theory Complete_Partial_Order2 provides reasoning
support for monotonicity and continuity in chain-complete partial orders
and about admissibility conditions for fixpoint inductions.
* Session HOL-Library: theory Library/Polynomial contains also
derivation of polynomials (formerly in Library/Poly_Deriv) but not
gcd/lcm on polynomials over fields. This has been moved to a separate
theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
future different type class instantiation for polynomials over factorial
rings. INCOMPATIBILITY.
* Session HOL-Library: theory Sublist provides function "prefixes" with
the following renaming
prefixeq -> prefix
prefix -> strict_prefix
suffixeq -> suffix
suffix -> strict_suffix
Added theory of longest common prefixes.
* Session HOL-Number_Theory: algebraic foundation for primes:
Generalisation of predicate "prime" and introduction of predicates
"prime_elem", "irreducible", a "prime_factorization" function, and the
"factorial_ring" typeclass with instance proofs for nat, int, poly. Some
theorems now have different names, most notably "prime_def" is now
"prime_nat_iff". INCOMPATIBILITY.
* Session Old_Number_Theory has been removed, after porting remaining
theories.
* Session HOL-Types_To_Sets provides an experimental extension of
Higher-Order Logic to allow translation of types to sets.
*** ML ***
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
library (notably for big integers). Subtle change of semantics:
Integer.gcd and Integer.lcm both normalize the sign, results are never
negative. This coincides with the definitions in HOL/GCD.thy.
INCOMPATIBILITY.
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing. Standard operations on type Rat.rat are provided via ad-hoc
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
superseded by General.Div.
* ML antiquotation @{path} is superseded by @{file}, which ensures that
the argument is a plain file. Minor INCOMPATIBILITY.
* Antiquotation @{make_string} is available during Pure bootstrap --
with approximative output quality.
* Low-level ML system structures (like PolyML and RunCall) are no longer
exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
* The ML function "ML" provides easy access to run-time compilation.
This is particularly useful for conditional compilation, without
requiring separate files.
* Option ML_exception_debugger controls detailed exception trace via the
Poly/ML debugger. Relevant ML modules need to be compiled beforehand
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
debugger information requires consirable time and space: main
Isabelle/HOL with full debugger support may need ML_system_64.
* Local_Theory.restore has been renamed to Local_Theory.reset to
emphasize its disruptive impact on the cumulative context, notably the
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
only appropriate when targets are managed, e.g. starting from a global
theory and returning to it. Regular definitional packages should use
balanced blocks of Local_Theory.open_target versus
Local_Theory.close_target instead. Rare INCOMPATIBILITY.
* Structure TimeLimit (originally from the SML/NJ library) has been
replaced by structure Timeout, with slightly different signature.
INCOMPATIBILITY.
* Discontinued cd and pwd operations, which are not well-defined in a
multi-threaded environment. Note that files are usually located
relatively to the master directory of a theory (see also
File.full_path). Potential INCOMPATIBILITY.
* Binding.empty_atts supersedes Thm.empty_binding and
Attrib.empty_binding. Minor INCOMPATIBILITY.
*** System ***
* SML/NJ and old versions of Poly/ML are no longer supported.
* Poly/ML heaps now follow the hierarchy of sessions, and thus require
much less disk space.
* The Isabelle ML process is now managed directly by Isabelle/Scala, and
shell scripts merely provide optional command-line access. In
particular:
. Scala module ML_Process to connect to the raw ML process,
with interaction via stdin/stdout/stderr or in batch mode;
. command-line tool "isabelle console" as interactive wrapper;
. command-line tool "isabelle process" as batch mode wrapper.
* The executable "isabelle_process" has been discontinued. Tools and
prover front-ends should use ML_Process or Isabelle_Process in
Isabelle/Scala. INCOMPATIBILITY.
* New command-line tool "isabelle process" supports ML evaluation of
literal expressions (option -e) or files (option -f) in the context of a
given heap image. Errors lead to premature exit of the ML process with
return code 1.
* The command-line tool "isabelle build" supports option -N for cyclic
shuffling of NUMA CPU nodes. This may help performance tuning on Linux
servers with separate CPU/memory modules.
* System option "threads" (for the size of the Isabelle/ML thread farm)
is also passed to the underlying ML runtime system as --gcthreads,
unless there is already a default provided via ML_OPTIONS settings.
* System option "checkpoint" helps to fine-tune the global heap space
management of isabelle build. This is relevant for big sessions that may
exhaust the small 32-bit address space of the ML process (which is used
by default).
* System option "profiling" specifies the mode for global ML profiling
in "isabelle build". Possible values are "time", "allocations". The
command-line tool "isabelle profiling_report" helps to digest the
resulting log files.
* System option "ML_process_policy" specifies an optional command prefix
for the underlying ML process, e.g. to control CPU affinity on
multiprocessor systems. The "isabelle jedit" tool allows to override the
implicit default via option -p.
* Command-line tool "isabelle console" provides option -r to help to
bootstrapping Isabelle/Pure interactively.
* Command-line tool "isabelle yxml" has been discontinued.
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
Isabelle/ML or Isabelle/Scala.
* Many Isabelle tools that require a Java runtime system refer to the
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
depending on the underlying platform. The settings for "isabelle build"
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
discontinued. Potential INCOMPATIBILITY.
* The Isabelle system environment always ensures that the main
executables are found within the shell search $PATH: "isabelle" and
"isabelle_scala_script".
* Isabelle tools may consist of .scala files: the Scala compiler is
invoked on the spot. The source needs to define some object that extends
Isabelle_Tool.Body.
* File.bash_string, File.bash_path etc. represent Isabelle/ML and
Isabelle/Scala strings authentically within GNU bash. This is useful to
produce robust shell scripts under program control, without worrying
about spaces or special characters. Note that user output works via
Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
less versatile) operations File.shell_quote, File.shell_path etc. have
been discontinued.
* The isabelle_java executable allows to run a Java process within the
name space of Java and Scala components that are bundled with Isabelle,
but without the Isabelle settings environment.
* Isabelle/Scala: the SSH module supports ssh and sftp connections, for
remote command-execution and file-system access. This resembles
operations from module File and Isabelle_System to some extent. Note
that Path specifications need to be resolved remotely via
ssh.remote_path instead of File.standard_path: the implicit process
environment is different, Isabelle settings are not available remotely.
* Isabelle/Scala: the Mercurial module supports repositories via the
regular hg command-line interface. The repositroy clone and working
directory may reside on a local or remote file-system (via ssh
connection).
New in Isabelle2016 (February 2016)
-----------------------------------
*** General ***
* Eisbach is now based on Pure instead of HOL. Objects-logics may import
either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or
~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that
the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further
examples that do require HOL.
* Better resource usage on all platforms (Linux, Windows, Mac OS X) for
both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage.
* Former "xsymbols" syntax with Isabelle symbols is used by default,
without any special print mode. Important ASCII replacement syntax
remains available under print mode "ASCII", but less important syntax
has been removed (see below).
* Support for more arrow symbols, with rendering in LaTeX and Isabelle
fonts: \ \ \ \ \ \.
* Special notation \ for the first implicit 'structure' in the
context has been discontinued. Rare INCOMPATIBILITY, use explicit
structure name instead, notably in indexed notation with block-subscript
(e.g. \\<^bsub>A\<^esub>).
* The glyph for \ in the IsabelleText font now corresponds better to its
counterpart \ as quantifier-like symbol. A small diamond is available as
\; the old symbol \ loses this rendering and any special
meaning.
* Syntax for formal comments "-- text" now also supports the symbolic
form "\ text". Command-line tool "isabelle update_cartouches -c" helps
to update old sources.
* Toplevel theorem statements have been simplified as follows:
theorems ~> lemmas
schematic_lemma ~> schematic_goal
schematic_theorem ~> schematic_goal
schematic_corollary ~> schematic_goal
Command-line tool "isabelle update_theorems" updates theory sources
accordingly.
* Toplevel theorem statement 'proposition' is another alias for
'theorem'.
* The old 'defs' command has been removed (legacy since Isabelle2014).
INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or
deferred definitions require a surrounding 'overloading' block.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the source-level debugger of Poly/ML, to work with
Isabelle/ML and official Standard ML. Option "ML_debugger" and commands
'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
'SML_file_no_debug' control compilation of sources with or without
debugging information. The Debugger panel allows to set breakpoints (via
context menu), step through stopped threads, evaluate local ML
expressions etc. At least one Debugger view needs to be active to have
any effect on the running ML program.
* The State panel manages explicit proof state output, with dynamic
auto-update according to cursor movement. Alternatively, the jEdit
action "isabelle.update-state" (shortcut S+ENTER) triggers manual
update.
* The Output panel no longer shows proof state output by default, to
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or
enable option "editor_output_state".
* The text overview column (status of errors, warnings etc.) is updated
asynchronously, leading to much better editor reactivity. Moreover, the
full document node content is taken into account. The width of the
column is scaled according to the main text area font, for improved
visibility.
* The main text area no longer changes its color hue in outdated
situations. The text overview column takes over the role to indicate
unfinished edits in the PIDE pipeline. This avoids flashing text display
due to ad-hoc updates by auxiliary GUI components, such as the State
panel.
* Slightly improved scheduling for urgent print tasks (e.g. command
state output, interactive queries) wrt. long-running background tasks.
* Completion of symbols via prefix of \ or \<^name> or \name is
always possible, independently of the language context. It is never
implicit: a popup will show up unconditionally.
* Additional abbreviations for syntactic completion may be specified in
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
support for simple templates using ASCII 007 (bell) as placeholder.
* Symbols \, \, \, \, \, \, \, \ no longer provide abbreviations for
completion like "+o", "*o", ".o" etc. -- due to conflicts with other
ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
emphasized text style; the effect is visible in document output, not in
the editor.
* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
instead of former C+e LEFT.
* The command-line tool "isabelle jedit" and the isabelle.Main
application wrapper treat the default $USER_HOME/Scratch.thy more
uniformly, and allow the dummy file argument ":" to open an empty buffer
instead.
* New command-line tool "isabelle jedit_client" allows to connect to an
already running Isabelle/jEdit process. This achieves the effect of
single-instance applications seen on common GUI desktops.
* The default look-and-feel for Linux is the traditional "Metal", which
works better with GUI scaling for very high-resolution displays (e.g.
4K). Moreover, it is generally more robust than "Nimbus".
* Update to jedit-5.3.0, with improved GUI scaling and support of
high-resolution displays (e.g. 4K).
* The main Isabelle executable is managed as single-instance Desktop
application uniformly on all platforms: Linux, Windows, Mac OS X.
*** Document preparation ***
* Commands 'paragraph' and 'subparagraph' provide additional section
headings. Thus there are 6 levels of standard headings, as in HTML.
* Command 'text_raw' has been clarified: input text is processed as in
'text' (with antiquotations and control symbols). The key difference is
the lack of the surrounding isabelle markup environment in output.
* Text is structured in paragraphs and nested lists, using notation that
is similar to Markdown. The control symbols for list items are as
follows:
\<^item> itemize
\<^enum> enumerate
\<^descr> description
* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>\...\ is equivalent to @{name \...\} and
\...\ without control symbol is equivalent to @{cartouche \...\}.
\<^name> without following cartouche is equivalent to @{name}. The
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
standard LaTeX macros of the same names.
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
Consequently, \...\ without any decoration prints literal quasi-formal
text. Command-line tool "isabelle update_cartouches -t" helps to update
old sources, by approximative patching of the content of string and
cartouche tokens seen in theory sources.
* The @{text} antiquotation now ignores the antiquotation option
"source". The given text content is output unconditionally, without any
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
argument where they are really intended, e.g. @{text \"foo"\}. Initial
or terminal spaces are ignored.
* Antiquotations @{emph} and @{bold} output LaTeX source recursively,
adding appropriate text style markup. These may be used in the short
form \<^emph>\...\ and \<^bold>\...\.
* Document antiquotation @{footnote} outputs LaTeX source recursively,
marked as \footnote{}. This may be used in the short form \<^footnote>\...\.
* Antiquotation @{verbatim [display]} supports option "indent".
* Antiquotation @{theory_text} prints uninterpreted theory source text
(Isar outer syntax with command keywords etc.). This may be used in the
short form \<^theory_text>\...\. @{theory_text [display]} supports option "indent".
* Antiquotation @{doc ENTRY} provides a reference to the given
documentation, with a hyperlink in the Prover IDE.
* Antiquotations @{command}, @{method}, @{attribute} print checked
entities of the Isar language.
* HTML presentation uses the standard IsabelleText font and Unicode
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former
print mode "HTML" loses its special meaning.
*** Isar ***
* Local goals ('have', 'show', 'hence', 'thus') allow structured rule
statements like fixes/assumes/shows in theorem specifications, but the
notation is postfix with keywords 'if' (or 'when') and 'for'. For
example:
have result: "C x y"
if "A x" and "B y"
for x :: 'a and y :: 'a
The local assumptions are bound to the name "that". The result is
exported from context of the statement as usual. The above roughly
corresponds to a raw proof block like this:
{
fix x :: 'a and y :: 'a
assume that: "A x" "B y"
have "C x y"