# HG changeset patch
# User wenzelm
# Date 1616430788 -3600
# Node ID 8eeea9901897a21d49c673bbf70a5fbc8d5c73d0
# Parent  86b900eff9bf9f4f6786bf05655049c435274352
more NEWS;

diff -r 86b900eff9bf -r 8eeea9901897 NEWS
--- a/NEWS	Mon Mar 22 17:28:07 2021 +0100
+++ b/NEWS	Mon Mar 22 17:33:08 2021 +0100
@@ -880,8 +880,11 @@
 
 *** Document preparation ***
 
-* High-quality blackboard-bold symbols for A..Z, from font "txmia"
-(package "pxfonts").
+* More predefined symbols: \<interleave> \<sslash> (package "stmaryrd"), \<checkmark> \<crossmark> (package
+"pifont").
+
+* High-quality blackboard-bold symbols from font "txmia" (package
+"pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
 
 * Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
 are stripped from document output: the effect is to modify the semantic