--- a/src/Doc/System/Sessions.thy Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Doc/System/Sessions.thy Sat Feb 24 22:56:56 2024 +0100
@@ -662,7 +662,7 @@
turned into plain spaces (according to their formal width).
The syntax for patters follows regular expressions of the Java
- platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
+ platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
\<close>
subsubsection \<open>Examples\<close>