src/HOL/Induct/LFilter.ML
changeset 8671 6ce91a80f616
parent 7499 23e090051cb8
equal deleted inserted replaced
8670:d69616c74211 8671:6ce91a80f616