# HG changeset patch
# User wenzelm
# Date 1503997722 -7200
# Node ID 075bbb78d33c555b7a38f516304ee2be3a740e35
# Parent  4d9c4cb9e9a56e9699d637e3f9d15ce33b418c81
proper theory name;

diff -r 4d9c4cb9e9a5 -r 075bbb78d33c 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.