NEWS
changeset 66542 075bbb78d33c
parent 66541 4d9c4cb9e9a5
child 66563 87b9eb69d5ba
     1.1 --- a/NEWS	Tue Aug 29 07:27:10 2017 +0200
     1.2 +++ b/NEWS	Tue Aug 29 11:08:42 2017 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4  Residues. Definition changed so that "totient 1 = 1" in agreement with
     1.5  the literature. Minor INCOMPATIBILITY.
     1.6  
     1.7 -* New styles in theory Library/LaTeXsugar:
     1.8 +* New styles in theory "HOL-Library.LaTeXsugar":
     1.9    - "dummy_pats" for printing equations with "_" on the lhs;
    1.10    - "eta_expand" for printing eta-expanded terms.
    1.11