src/HOL/Induct/LFilter.ML
changeset 8262 08ad0a986db2
parent 7499 23e090051cb8