src/HOL/Hyperreal/NthRoot.thy
changeset 14898 a25550451b51
parent 14767 d2b071e65e4c
child 15085 5693a977a767