src/HOL/Induct/LFilter.ML
changeset 10499 2f33d0fd242e
parent 7499 23e090051cb8