Summary
- Merge
- partial tidy-up of Sylow's theorem
- proper option process_output_tail, more generous default;
The file was modified | src/HOL/Algebra/Exponent.thy (diff) |
The file was modified | src/HOL/Algebra/Sylow.thy (diff) |
The file was modified | src/HOL/Number_Theory/Primes.thy (diff) |
The file was modified | etc/options (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |