Skip to content
Success

Changes

Summary

  1. New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
Changeset 64919:7e0c8924dfda by paulson _lp15@cam.ac.uk_:
New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
The file was modified src/HOL/Library/Discrete.thy (diff)