src/HOL/Library/ContNotDenum.thy
changeset 54611 31afce809794
parent 54263 c4159fe6fa46
child 54797 be020ec8560c
equal deleted inserted replaced
54610:6593e06445e6 54611:31afce809794