src/HOL/ex/LList.thy
changeset 1868 836950047d85
parent 1824 44254696843a
child 2911 8a680e310f04