src/HOL/Filter.thy
changeset 67974 3f352a91b45a
parent 67956 79dbb9dccc99
child 68667 96aae7c44bb2