diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index d2e49d81783..a12d75eabbe 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -3,18 +3,18 @@
 
 stdenv.mkDerivation rec {
   pname = "isabelle";
-  version = "2018";
+  version = "2020";
 
   dirname = "Isabelle${version}";
 
   src = if stdenv.isDarwin
     then fetchurl {
-      url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg";
-      sha256 = "0jwnvsf5whklq14ihaxs7b9nbic94mm56nvxljrdbvl6y628j9r5";
+      url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz";
+      sha256 = "1sfr5filsaqj93g5y4p9n8g5652dhr4whj25x4lifdxr2pp560xx";
     }
     else fetchurl {
       url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz";
-      sha256 = "1928lwrw1v1p9s23kix30ncpqm8djmrnjixj82f3ni2a8sc3hrsp";
+      sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3";
     };
 
   buildInputs = [ perl polyml z3 ]
@@ -42,14 +42,14 @@ stdenv.mkDerivation rec {
       ML_SOURCES="\$POLYML_HOME/src"
     EOF
 
-    cat >contrib/jdk/etc/settings <<EOF
+    cat >contrib/jdk*/etc/settings <<EOF
       ISABELLE_JAVA_PLATFORM=${stdenv.system}
       ISABELLE_JDK_HOME=${java}
     EOF
 
     echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings
 
-    for comp in contrib/jdk contrib/polyml-* contrib/z3-*; do
+    for comp in contrib/jdk* contrib/polyml-* contrib/z3-*; do
       rm -rf $comp/x86*
     done
     '' + (if ! stdenv.isLinux then "" else ''
@@ -66,7 +66,7 @@ stdenv.mkDerivation rec {
     bin/isabelle install $out/bin
   '';
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "A generic proof assistant";
 
     longDescription = ''
@@ -74,9 +74,9 @@ stdenv.mkDerivation rec {
       to be expressed in a formal language and provides tools for proving those
       formulas in a logical calculus.
     '';
-    homepage = "http://isabelle.in.tum.de/";
-    license = "LGPL";
-    maintainers = [ stdenv.lib.maintainers.jwiegley ];
-    platforms = stdenv.lib.platforms.linux;
+    homepage = "https://isabelle.in.tum.de/";
+    license = licenses.bsd3;
+    maintainers = [ maintainers.jwiegley ];
+    platforms = platforms.linux;
   };
 }
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index ffbe244d89b..56792c2e612 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -25827,11 +25827,11 @@ in
   ifstat-legacy = callPackage ../tools/networking/ifstat-legacy { };
 
   isabelle = callPackage ../applications/science/logic/isabelle {
-    polyml = stdenv.lib.overrideDerivation polyml57 (attrs: {
+    polyml = stdenv.lib.overrideDerivation polyml (attrs: {
       configureFlags = [ "--enable-intinf-as-int" "--with-gmp" "--disable-shared" ];
     });
 
-    java = if stdenv.isLinux then jre else jdk;
+    java = openjdk11;
   };
 
   iprover = callPackage ../applications/science/logic/iprover { };