--- a/.hgtags Mon Nov 30 11:06:13 2020 +0000
+++ b/.hgtags Mon Nov 30 19:33:07 2020 +0000
@@ -37,3 +37,4 @@
91162dd89571fb9ddfa36844fdb1a16aea13adcf Isabelle2018
83774d669b5181fb28d19d7a0219fbf6c6d38aab Isabelle2019
abf3e80bd815c2c062b02c78b256f7ba27481380 Isabelle2020
+21ff9c1a464494b3a61c3538650664cc1b42c0cb Isabelle2021-RC0
--- a/Admin/Release/CHECKLIST Mon Nov 30 11:06:13 2020 +0000
+++ b/Admin/Release/CHECKLIST Mon Nov 30 19:33:07 2020 +0000
@@ -45,8 +45,6 @@
- check doc/Contents, src/Tools/jEdit/dist/doc/Contents;
-- check "Handler catches all exceptions"
-
- test old HD display: Linux, Windows, Mac OS X;
- Mac OS X: check recent MacTeX;
--- a/Admin/components/bundled-windows Mon Nov 30 11:06:13 2020 +0000
+++ b/Admin/components/bundled-windows Mon Nov 30 19:33:07 2020 +0000
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20201002
+cygwin-20201130
windows_app-20181006
--- a/Admin/components/components.sha1 Mon Nov 30 11:06:13 2020 +0000
+++ b/Admin/components/components.sha1 Mon Nov 30 19:33:07 2020 +0000
@@ -62,6 +62,7 @@
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
@@ -185,6 +186,7 @@
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
@@ -276,6 +278,7 @@
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
@@ -323,6 +326,7 @@
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
--- a/Admin/components/main Mon Nov 30 11:06:13 2020 +0000
+++ b/Admin/components/main Mon Nov 30 19:33:07 2020 +0000
@@ -7,19 +7,19 @@
isabelle_fonts-20190717
jdk-11.0.9+11
jedit_build-20200908
-jfreechart-1.5.0
+jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6
nunchaku-0.5
opam-2.0.7
polyml-test-f86ae3dc1686
-postgresql-42.2.9
+postgresql-42.2.18
scala-2.12.12
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.32.3.2
ssh-java-20190323
-stack-2.1.3
+stack-2.5.1
vampire-4.2.2
xz-java-1.8
verit-2020.10-rmx-1
--- a/etc/settings Mon Nov 30 11:06:13 2020 +0000
+++ b/etc/settings Mon Nov 30 19:33:07 2020 +0000
@@ -158,9 +158,9 @@
ISABELLE_STACK_ROOT="$USER_HOME/.stack"
-ISABELLE_STACK_RESOLVER="lts-13.19"
+ISABELLE_STACK_RESOLVER="lts-16.12"
-ISABELLE_GHC_VERSION="ghc-8.6.4"
+ISABELLE_GHC_VERSION="ghc-8.8.4"
###
--- a/src/HOL/Library/Bit_Operations.thy Mon Nov 30 11:06:13 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Mon Nov 30 19:33:07 2020 +0000
@@ -161,7 +161,7 @@
lemma or_eq_0_iff:
\<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
- by (auto simp add: bit_eq_iff bit_or_iff)
+ by (auto simp add: bit_eq_iff bit_or_iff)
lemma disjunctive_add:
\<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
@@ -269,7 +269,7 @@
proof
assume \<open>a = - 1 \<and> b = - 1\<close>
then show \<open>a AND b = - 1\<close>
- by simp
+ by simp
next
assume \<open>a AND b = - 1\<close>
have *: \<open>bit a n\<close> \<open>bit b n\<close> if \<open>2 ^ n \<noteq> 0\<close> for n
@@ -278,7 +278,7 @@
have \<open>bit (a AND b) n = bit (- 1) n\<close>
by (simp add: bit_eq_iff)
then show \<open>bit a n\<close> \<open>bit b n\<close>
- using that by (simp_all add: bit_and_iff)
+ using that by (simp_all add: bit_and_iff)
qed
have \<open>a = - 1\<close>
by (rule bit_eqI) (simp add: *)
--- a/src/HOL/Library/Type_Length.thy Mon Nov 30 11:06:13 2020 +0000
+++ b/src/HOL/Library/Type_Length.thy Mon Nov 30 19:33:07 2020 +0000
@@ -113,7 +113,7 @@
lemma two_less_eq_exp_length [simp]:
\<open>2 \<le> 2 ^ LENGTH('b::len)\<close>
using mult_left_mono [of 1 \<open>2 ^ (LENGTH('b::len) - 1)\<close> 2]
- by (cases \<open>LENGTH('b::len)\<close>) simp_all
+ by (cases \<open>LENGTH('b::len)\<close>) simp_all
end
--- a/src/HOL/Parity.thy Mon Nov 30 11:06:13 2020 +0000
+++ b/src/HOL/Parity.thy Mon Nov 30 19:33:07 2020 +0000
@@ -1197,7 +1197,7 @@
lemma bit_of_bool_iff [bit_simps]:
\<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
- by (simp add: bit_1_iff)
+ by (simp add: bit_1_iff)
lemma even_of_nat_iff:
\<open>even (of_nat n) \<longleftrightarrow> even n\<close>
@@ -1536,7 +1536,7 @@
proof
assume ?P
then show ?Q
- by (simp add: take_bit_eq_mod mod_0_imp_dvd)
+ by (simp add: take_bit_eq_mod mod_0_imp_dvd)
next
assume ?Q
then obtain b where \<open>a = push_bit n b\<close>