NEWS
changeset 66541 4d9c4cb9e9a5
parent 66488 9d83e8fe3de3
child 66542 075bbb78d33c
     1.1 --- a/NEWS	Mon Aug 28 22:32:22 2017 +0100
     1.2 +++ b/NEWS	Tue Aug 29 07:27:10 2017 +0200
     1.3 @@ -212,6 +212,10 @@
     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 +  - "dummy_pats" for printing equations with "_" on the lhs;
     1.9 +  - "eta_expand" for printing eta-expanded terms.
    1.10 +
    1.11  * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
    1.12  been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
    1.13