src/HOL/Archimedean_Field.thy
changeset 80988 f1991616c5c3
parent 80932 261cd8722677
child 81125 ec121999a9cb