Summary
- Fixed import path in Factorial_Ring
- Merged
- Merged
- Tuned
- Merged
- moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
- moved material from AFP to distribution
The file was modified | src/HOL/Number_Theory/Factorial_Ring.thy (diff) |
The file was modified | src/HOL/Library/Formal_Power_Series.thy (diff) |
The file was modified | src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff) |
The file was modified | src/HOL/Number_Theory/Factorial_Ring.thy (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/Formal_Power_Series.thy (diff) |
The file was modified | src/HOL/Analysis/Harmonic_Numbers.thy (diff) |
The file was modified | src/HOL/Probability/Probability_Mass_Function.thy (diff) |
The file was modified | src/HOL/Probability/Random_Permutations.thy (diff) |