src/HOL/Hyperreal/NthRoot.thy
changeset 23247 b99dce43d252
parent 23122 3d853d6f2f7d
child 23257 9117e228a8e3