src/HOL/Hyperreal/Filter.thy
changeset 18117 61a430a67d7c
parent 17332 4910cf8c0cd2
child 19931 fb32b43e7f80
equal deleted inserted replaced
18116:92c98f31f82d 18117:61a430a67d7c