src/HOL/Induct/LFilter.ML
changeset 11649 dfb59b9954a6
parent 7499 23e090051cb8