src/HOL/Library/Coinductive_List.thy
changeset 30705 e8ab35c6ade6
parent 30663 0b6aff7451b2
child 30952 7ab2716dd93b