src/HOL/Library/Diagonalize.thy
2009-03-06 haftmann 2009-03-06 constructive version of Cantor's first diagonalization argument