Summary
- tuned
- more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function
The file was modified | src/HOL/Conditionally_Complete_Lattices.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was added | src/HOL/Number_Theory/Totient.thy |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Number_Theory/Euler_Criterion.thy (diff) |
The file was modified | src/HOL/Number_Theory/Pocklington.thy (diff) |
The file was modified | src/HOL/Number_Theory/Residues.thy (diff) |