src/HOL/Induct/LList.thy
changeset 9714 79db0e5b7824
parent 6382 8b0c9205da75
child 10834 a7897aebbffc