src/HOL/Induct/LFilter.ML
changeset 10961 74817560a8e8
parent 7499 23e090051cb8