src/HOL/Filter.thy
changeset 79714 80cb54976c1c
parent 79530 1b0fc6ceb750
child 80175 200107cdd3ac