src/HOL/Filter.thy
changeset 71989 bad75618fb82
parent 71743 0239bee6bffd
child 74325 8d0c2d74ad63
equal deleted inserted replaced
71988:ace45a11a45e 71989:bad75618fb82