src/HOL/Induct/LFilter.ML
changeset 3776 38f8ec304b95
parent 3724 f33e301a89f5
child 3842 b55686a7b22c