src/HOL/Hyperreal/Series.thy
changeset 27364 a8672b0e2b15
parent 27108 e447b3107696