src/HOL/Filter.thy
changeset 72470 e2e9ef9aa2df
parent 71743 0239bee6bffd
child 74325 8d0c2d74ad63
equal deleted inserted replaced
72459:15fc6320da68 72470:e2e9ef9aa2df