Summary
- merged
- small tidy-up of Complex_Transcendental
- merged
- small clean-up of Complex_Analysis_Basics
- more complete and more correct documentation on code generation
- grouped material on numeral division
- automatic classical rule to derive a dvd b from b mod a = 0
- consider dvdE for automated classical proving
The file was modified | src/HOL/Analysis/Complex_Transcendental.thy (diff) |
The file was modified | src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff) |
The file was modified | src/HOL/Analysis/Complex_Analysis_Basics.thy (diff) |
The file was modified | src/HOL/Analysis/Complex_Transcendental.thy (diff) |
The file was modified | src/HOL/Analysis/Conformal_Mappings.thy (diff) |
The file was modified | src/HOL/Analysis/Great_Picard.thy (diff) |
The file was modified | src/Doc/Codegen/Foundations.thy (diff) |
The file was modified | src/Doc/Isar_Ref/HOL_Specific.thy (diff) |
The file was modified | src/HOL/Divides.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |
The file was modified | src/HOL/Rings.thy (diff) |