Summary
- tuned
- clarified theory name; tuned;
- New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
The file was modified | src/HOL/Library/Tree.thy (diff) |
The file was added | src/HOL/ex/Peano_Axioms.thy |
The file was modified | src/HOL/ROOT (diff) |
The file was removed | src/HOL/ex/Abstract_NAT.thy |
The file was modified | src/HOL/Library/Discrete.thy (diff) |