src/ZF/add_ind_def.thy
changeset 4930 89271bc4e7ed
parent 1735 96244c247b07