src/HOL/Filter.thy
changeset 72219 0f38c96a0a74
parent 71743 0239bee6bffd
child 74325 8d0c2d74ad63
equal deleted inserted replaced
72211:a6cbf8ce979e 72219:0f38c96a0a74