diff -r aa77ebb2dc16 -r 54d0f6edfe3a src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Feb 24 22:15:42 2024 +0100
+++ b/src/Doc/System/Server.thy	Sat Feb 24 22:56:56 2024 +0100
@@ -491,7 +491,7 @@
 
   \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
   as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
-  \<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
+  \<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/UUID.html\<close>.\<close> Such
   identifiers are created as private random numbers of the server and only
   revealed to the client that creates a certain resource (e.g.\ task or
   session). A client may disclose this information for use in a different