src/HOL/Induct/LFilter.ML
changeset 6095 9f75a45384dd
parent 5618 721671c68324
child 6141 a6922171b396