src/HOL/Datatype.thy
changeset 21083 a1de02f047d0
parent 21079 747d716e98d0
child 21111 624ed9c7c4fe