src/HOL/Induct/LList.thy
changeset 10168 50be659d4222
parent 6382 8b0c9205da75
child 10834 a7897aebbffc