src/HOL/Complex/ex/DenumRat.thy
changeset 22893 1b0f4e6f81aa
parent 19108 6f8c1343341b
child 28098 c92850d2d16c