src/HOL/Induct/LFilter.thy
changeset 12600 30ec65eaaf5f
parent 9101 b643f4d7b9e9
child 13075 d3e1d554cd6d