src/HOL/Filter.thy
changeset 76285 8e777e0e206a
parent 74325 8d0c2d74ad63
child 76722 b1d57dd345e1
equal deleted inserted replaced
76284:71bf371a9784 76285:8e777e0e206a