src/HOL/Hyperreal/Filter.thy
changeset 18780 a9c38d41cd27
parent 17332 4910cf8c0cd2
child 19931 fb32b43e7f80
equal deleted inserted replaced
18779:a9f41c380b2f 18780:a9c38d41cd27