src/HOL/Library/ContNotDenum.thy
changeset 54611 31afce809794
parent 54263 c4159fe6fa46
child 54797 be020ec8560c