diff --git a/sci-mathematics/isabelle-bin/Manifest b/sci-mathematics/isabelle-bin/Manifest
new file mode 100644
index 0000000..3423a22
--- /dev/null
+++ b/sci-mathematics/isabelle-bin/Manifest
@@ -0,0 +1 @@
+DIST isabelle-bin-2021.tar.gz 483561674 BLAKE2B 00390c785a858637918847821f4a429853b7ce968a8d71a37c3b6ac392438577ff3241f106840054eeadda19621a0ccd6afc9fce282720383657f28f304ed0ed SHA512 5a91f867bc743f6bcfca87fb04f4d2ca20570545bcfab6150a8f3516efd00abac7f9346f69b6f53988ca39053d78feae92e10a00a0453f2300280797a2c14b85
diff --git a/sci-mathematics/isabelle-bin/isabelle-bin-2021.ebuild b/sci-mathematics/isabelle-bin/isabelle-bin-2021.ebuild
new file mode 100644
index 0000000..961d71a
--- /dev/null
+++ b/sci-mathematics/isabelle-bin/isabelle-bin-2021.ebuild
@@ -0,0 +1,50 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit desktop wrapper xdg
+
+MY_P="Isabelle${PV}"
+
+DESCRIPTION="Generic proof assistant with higher-order logic"
+HOMEPAGE="https://isabelle.in.tum.de/overview.html"
+SRC_URI="https://isabelle.in.tum.de/dist/${MY_P}_linux.tar.gz -> ${P}.tar.gz"
+S="${WORKDIR}/${MY_P}"
+
+RESTRICT="bindist test"
+LICENSE="BSD"
+SLOT="0/${PV}"
+KEYWORDS="-* ~amd64"
+
+RDEPEND="
+	!sci-mathematics/isabelle
+"
+
+QA_PREBUILT=".*"
+
+src_install() {
+	local ISABELLE_HOME="/opt/isabelle"
+
+	local doc
+	for doc in ANNOUNCE CONTRIBUTORS COPYRIGHT NEWS README; do
+		if [[ -f ${doc} ]]; then
+			dodoc ${doc}
+			rm ${doc} || die
+		fi
+	done
+
+	mkdir -p "${ED}/${ISABELLE_HOME}" || die
+	cp -r ./* "${ED}/${ISABELLE_HOME}" || die
+
+	local isabelle_env='env USER_HOME=${HOME}/.cache/isabelle'
+	local wrap
+	for wrap in ${PN} ${MY_P} Isabelle isabelle; do
+		make_wrapper ${wrap} "${isabelle_env} ${ISABELLE_HOME}/${MY_P}" "${ISABELLE_HOME}"
+	done
+
+	doicon ./lib/icons/isabelle-mini.xpm
+	doicon ./lib/icons/isabelle.xpm
+
+	make_desktop_entry isabelle Isabelle isabelle "Education;Science;Math;"
+}
diff --git a/sci-mathematics/isabelle-bin/metadata.xml b/sci-mathematics/isabelle-bin/metadata.xml
new file mode 100644
index 0000000..aef054f
--- /dev/null
+++ b/sci-mathematics/isabelle-bin/metadata.xml
@@ -0,0 +1,14 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <longdescription lang="en">
+    Isabelle is a generic proof assistant. It allows mathematical formulas
+    to be expressed in a formal language and provides tools for proving
+    those formulas in a logical calculus. Isabelle was originally developed
+    at the University of Cambridge and Technische Universität München,
+    but now includes numerous contributions from institutions
+    and individuals worldwide.
+    See the Isabelle overview for a brief introduction.
+  </longdescription>
+</pkgmetadata>