src/HOL/Library/Old_Datatype.thy
changeset 62379 340738057c8c
parent 62145 5b946c81dfbf
child 65513 587433a18053