src/HOL/Hyperreal/Series.thy
changeset 12130 30d9143aff7e
parent 12018 ec054019c910
child 14416 1f256287d4f0
equal deleted inserted replaced
12129:964f5ffe13d0 12130:30d9143aff7e