src/HOL/Induct/LList.thy
changeset 5191 8ceaa19f7717
parent 3842 b55686a7b22c
child 5977 9f0c8869cf71