NEWS

--- a/NEWS	Tue Aug 29 07:27:10 2017 +0200
+++ b/NEWS	Tue Aug 29 11:08:42 2017 +0200
@@ -212,7 +212,7 @@
 Residues. Definition changed so that "totient 1 = 1" in agreement with
 the literature. Minor INCOMPATIBILITY.
 
-* New styles in theory Library/LaTeXsugar:
+* New styles in theory "HOL-Library.LaTeXsugar":
   - "dummy_pats" for printing equations with "_" on the lhs;
   - "eta_expand" for printing eta-expanded terms.