src/HOL/Induct/LFilter.thy
changeset 13286 a7f0f8869b54
parent 13107 8743cc847224
child 13612 55d32e76ef4e