Summary
- A bit of cleaning up
- The same, without adding a new simprule
- moved some material from Sum_of_Powers
The file was modified | src/HOL/Nonstandard_Analysis/CLim.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/HSeries.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/HTranscendental.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/HyperDef.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/NSA.thy (diff) |
The file was modified | src/HOL/Binomial.thy (diff) |
The file was modified | src/HOL/Factorial.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |
The file was modified | src/HOL/Binomial.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |
The file was modified | src/HOL/Real.thy (diff) |
The file was modified | src/HOL/ex/Sum_of_Powers.thy (diff) |