src/HOL/Induct/LList.thy
changeset 7333 6cb15c6f1d9f
parent 6382 8b0c9205da75
child 10834 a7897aebbffc