src/HOL/Library/Discrete_Functions.thy
changeset 82775 61c39a9e5415
parent 82664 e9f3b94eb6a0