src/HOL/Hyperreal/NthRoot.thy
changeset 25722 0a104ddb72d9
parent 25602 137ebc0603f4
child 25766 6960410f134d