src/HOL/Induct/LFilter.ML
changeset 4332 d4a15e32c024
parent 4090 9f1eaab75e8c
child 4477 b3e5857d8d99