Skip to content
Success

Changes

Summary

  1. tuned
  2. clarified theory name; tuned;
  3. New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
Changeset 64921:1cbfe46ad6b1 by nipkow:
tuned
The file was modified src/HOL/Library/Tree.thy (diff)
Changeset 64920:31044168af84 by wenzelm:
clarified theory name;<br>tuned;
The file was addedsrc/HOL/ex/Peano_Axioms.thy
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/ex/Abstract_NAT.thy
Changeset 64919:7e0c8924dfda by paulson _lp15@cam.ac.uk_:
New material from Bertrand&#039;s postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
The file was modified src/HOL/Library/Discrete.thy (diff)