src/HOL/Induct/LFilter.ML
changeset 6105 b4ec1af7053f
parent 5618 721671c68324
child 6141 a6922171b396
equal deleted inserted replaced
6104:55c7f8f0bb4d 6105:b4ec1af7053f