src/HOL/Filter.thy
changeset 73616 b0ea03e837b1
parent 71743 0239bee6bffd
child 74325 8d0c2d74ad63
equal deleted inserted replaced
73615:e768759ce6c5 73616:b0ea03e837b1