src/HOL/Library/Discrete.thy
changeset 64582 3d20ded18f14
parent 64449 8c44dfb4ca8a
child 64919 7e0c8924dfda