src/ZF/add_ind_def.thy
changeset 4552 bb8ff763c93d
parent 1735 96244c247b07