src/HOL/Hyperreal/NthRoot.thy
changeset 23024 70435ffe077d
parent 23009 01c295dd4a36
child 23042 492514b39956