src/HOL/Datatype.thy
changeset 28973 c549650d1442
parent 28689 2947dc320178
child 29025 8c8859c0d734