src/HOL/Filter.thy
changeset 61944 5d06ecfdb472
parent 61841 4d3527b94f2a
child 61953 7247cb62406c