src/HOL/Filter.thy
changeset 64877 31e9920a0dc1
parent 63967 2aa42596edc3
child 65578 e4997c181cce
equal deleted inserted replaced
64876:65a247444100 64877:31e9920a0dc1