src/HOL/Library/Discrete.thy
changeset 64684 fe2c9c215b36
parent 64449 8c44dfb4ca8a
child 64919 7e0c8924dfda