diff -r 8fb3b3a10667 -r b8ee1ef948c2 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Aug 20 14:55:21 2022 +0200
+++ b/src/Pure/General/path.scala	Sat Aug 20 16:32:18 2022 +0200
@@ -91,6 +91,8 @@
   val USER_HOME: Path = variable("USER_HOME")
   val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
 
+  val index_html: Path = basic("index.html")
+
 
   /* explode */
 
@@ -158,6 +160,10 @@
       error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n  "))
     }
   }
+
+  def eq_case_insensitive(path1: Path, path2: Path): Boolean =
+    path1 == path2 ||
+    Word.lowercase(path1.expand.implode) == Word.lowercase(path2.expand.implode)
 }