src/HOL/Filter.thy
changeset 80753 66893c47500d
parent 80612 e65eed943bee
child 80760 be8c0e039a5e