src/HOL/Library/Discrete.thy
changeset 63794 bcec0534aeea
parent 63766 695d60817cb1
child 64449 8c44dfb4ca8a