NEWS
changeset 59899 91f4f956b1eb
parent 59892 2a616319c171
child 59901 840d03805755
equal deleted inserted replaced
59898:81c70bdbd908 59899:91f4f956b1eb
   326 * Document antiquotation @{verbatim} prints ASCII text literally in "tt"
   326 * Document antiquotation @{verbatim} prints ASCII text literally in "tt"
   327 style.
   327 style.
   328 
   328 
   329 
   329 
   330 *** ML ***
   330 *** ML ***
       
   331 
       
   332 * Subtle change of name space policy: undeclared entries are now
       
   333 considered inaccessible, instead of accessible via the fully-qualified
       
   334 internal name. This mainly affects Name_Space.intern (and derivatives),
       
   335 which may produce an unexpected Long_Name.hidden prefix. Note that
       
   336 contempory applications use the strict Name_Space.check (and
       
   337 derivatives) instead, which is not affected by the change. Potential
       
   338 INCOMPATIBILITY in rare applications of Name_Space.intern.
   331 
   339 
   332 * The main operations to certify logical entities are Thm.ctyp_of and
   340 * The main operations to certify logical entities are Thm.ctyp_of and
   333 Thm.cterm_of with a local context; old-style global theory variants are
   341 Thm.cterm_of with a local context; old-style global theory variants are
   334 available as Thm.global_ctyp_of and Thm.global_cterm_of.
   342 available as Thm.global_ctyp_of and Thm.global_cterm_of.
   335 INCOMPATIBILITY.
   343 INCOMPATIBILITY.