src/HOL/Analysis/Continuum_Not_Denumerable.thy
changeset 74811 1f40ded31b78
parent 70136 f03a01a18c6e
child 75078 ec86cb2418e1