src/HOL/Library/Discrete.thy
changeset 64722 6df73de0d3c7
parent 64449 8c44dfb4ca8a
child 64919 7e0c8924dfda