src/HOL/Archimedean_Field.thy
changeset 82584 7ab0fb5d9919
parent 82542 32a6228f543d
child 82689 817f97d8cd26