diff -r 6157757bb133 -r 5924c1da3c45 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Aug 27 12:43:06 2020 +0200
+++ b/src/Pure/library.scala	Thu Aug 27 12:51:57 2020 +0200
@@ -276,4 +276,20 @@
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
+
+
+  /* reflection */
+
+  def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
+  {
+    @tailrec def subclass(c: Class[_]): Boolean =
+    {
+      c == b ||
+        {
+          val d = c.getSuperclass
+          d != null && subclass(d)
+        }
+    }
+    subclass(a)
+  }
 }