src/HOL/Filter.thy
changeset 80753 66893c47500d
parent 80612 e65eed943bee
child 80760 be8c0e039a5e
equal deleted inserted replaced
80752:2c9b5288eb84 80753:66893c47500d