src/HOL/Induct/LFilter.thy
changeset 33693 9d76c8080aea
parent 32960 69916a850301