NEWS
changeset 59621 291934bac95e
parent 59588 c6f3dbe466b6
child 59648 d1148f0baef5
--- a/NEWS	Fri Mar 06 14:01:08 2015 +0100
+++ b/NEWS	Fri Mar 06 15:58:56 2015 +0100
@@ -263,6 +263,11 @@
 
 *** ML ***
 
+* The main operations to certify logical entities are Thm.ctyp_of and
+Thm.cterm_of with a local context; old-style global theory variants are
+available as Thm.global_ctyp_of and Thm.global_cterm_of.
+INCOMPATIBILITY.
+
 * Elementary operations in module Thm are no longer pervasive.
 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
 Thm.term_of etc.