src/HOL/Library/Discrete.thy
changeset 81466 bb82ebb18b5d
parent 81332 f94b30fa2b6c