src/HOL/Filter.thy
changeset 64715 33d5fa0ce6e5
parent 63967 2aa42596edc3
child 65578 e4997c181cce