src/HOL/Filter.thy
changeset 60614 e39e6881985c
parent 60589 b5622eef7176
child 60721 c1b7793c23a3
equal deleted inserted replaced
60613:f11e9fd70b7d 60614:e39e6881985c