src/HOL/Archimedean_Field.thy
changeset 56730 e723f041b6d0
parent 54489 03ff4d1e6784
child 58040 9a867afaab5a