changeset 17869 | 585c1f08499e |
parent 17865 | 5b0c3dcfbad2 |
child 17878 | 5b9efe4d6b47 |
--- a/NEWS Sat Oct 15 00:09:20 2005 +0200 +++ b/NEWS Sat Oct 15 00:14:30 2005 +0200 @@ -11,8 +11,8 @@ *** Document preparation *** -* Added antiquotations @{ML_type text} and @{ML_struct} which check -the given source text as ML type/structure, printing verbatim. +* Added antiquotations @{ML_type text} and @{ML_struct text} which +check the given source text as ML type/structure, printing verbatim. *** Pure ***