src/HOL/Induct/LFilter.ML
changeset 6538 d575fb1edabf
parent 6141 a6922171b396
child 7499 23e090051cb8
equal deleted inserted replaced
6537:b1288c5e599c 6538:d575fb1edabf