src/HOL/Induct/LList.thy
changeset 6095 9f75a45384dd
parent 5977 9f0c8869cf71
child 6382 8b0c9205da75