src/HOL/Library/Discrete.thy
changeset 80914 d97fdabd9e2b
parent 80621 6c369fec315a
child 81332 f94b30fa2b6c