src/HOL/Filter.thy
changeset 67623 dee9d2924617
parent 67613 ce654b0e6d69
child 67616 1d005f514417
equal deleted inserted replaced
67622:5289d3bdb261 67623:dee9d2924617