src/HOL/Hyperreal/NthRoot.thy
changeset 18396 b3e7da94b51f
parent 16775 c1b87ef4a1c3
child 18585 5d379fe2eb74