src/HOL/Archimedean_Field.thy
changeset 56346 42533f8f4729
parent 54489 03ff4d1e6784
child 58040 9a867afaab5a