src/HOL/Hyperreal/Series.thy
changeset 23024 70435ffe077d
parent 22998 97e1f9c2cc46
child 23084 bc000fc64fce