equal
deleted
inserted
replaced
209 |
209 |
210 * Theory "Number_Theory.Totient" introduces basic notions about Euler's |
210 * Theory "Number_Theory.Totient" introduces basic notions about Euler's |
211 totient function previously hidden as solitary example in theory |
211 totient function previously hidden as solitary example in theory |
212 Residues. Definition changed so that "totient 1 = 1" in agreement with |
212 Residues. Definition changed so that "totient 1 = 1" in agreement with |
213 the literature. Minor INCOMPATIBILITY. |
213 the literature. Minor INCOMPATIBILITY. |
|
214 |
|
215 * New styles in theory Library/LaTeXsugar: |
|
216 - "dummy_pats" for printing equations with "_" on the lhs; |
|
217 - "eta_expand" for printing eta-expanded terms. |
214 |
218 |
215 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has |
219 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has |
216 been renamed to bij_swap_compose_bij. INCOMPATIBILITY. |
220 been renamed to bij_swap_compose_bij. INCOMPATIBILITY. |
217 |
221 |
218 * New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" |
222 * New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" |