src/HOL/Induct/LList.thy
changeset 9772 c07777210a69
parent 6382 8b0c9205da75
child 10834 a7897aebbffc