Document the new incompatibilities in DB.{find,match}

HOL-Theorem-Prover · Nov 14, 2024 · b9744e3 · b9744e3
1 parent fbf5560
commit b9744e3
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/doc/next-release.md b/doc/next-release.md
@@ -74,6 +74,16 @@ Incompatibilities:
            (load "<path>/HOL/tools/editor-modes/emacs/hol-mode")
            (load "<path>/HOL/tools/editor-modes/emacs/hol-unicode")
 
+-   The types of `DB.find` and `DB.match` have changed so that instead of returning
+
+           (string * string) * (thm * class)
+
+    they now return
+
+           (string * string) * (thm * class * thm_src_location)
+
+    Using the `#1 o #2` selector should be future-proof here.
+
 
 * * * * *