src/ZF/add_ind_def.thy
changeset 3991 4cb2f2422695
parent 1735 96244c247b07