src/HOL/Filter.thy
changeset 80726 5f13872a33ea
parent 80612 e65eed943bee
child 80760 be8c0e039a5e
equal deleted inserted replaced
80725:ea8d52d37313 80726:5f13872a33ea