src/HOL/Archimedean_Field.thy
changeset 77050 92509e4274eb
parent 75878 fcd118d9242f
child 77490 2c86ea8961b5