--- a/NEWS Tue Sep 21 12:35:38 2021 +0200
+++ b/NEWS Tue Sep 21 13:12:14 2021 +0200
@@ -262,6 +262,10 @@
* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
corresponding ML values, notably as arguments for Thm.instantiate etc.
+* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
+corresponding functions for the object-logic of the ML compilation
+context. This supersedes older mk_Trueprop / dest_Trueprop operations.
+
* ML antiquotations for type constructors and term constants:
\<^Type>\<open>c\<close>