src/HOL/Library/Coinductive_List.thy
changeset 25920 8df5eabda5f6
parent 25595 6c48275f9c76
child 27368 9f90ac19e32b