src/HOL/Datatype.thy
changeset 54861 00d551179872
parent 54398 100c0eaf63d5
child 55415 05f5fdb8d093