src/HOL/Library/Discrete.thy
changeset 80889 510f6cb6721e
parent 80621 6c369fec315a
child 81332 f94b30fa2b6c
equal deleted inserted replaced
80888:c5ea0cb4dd91 80889:510f6cb6721e