src/ZF/Inductive.thy
changeset 583 550292083e66
parent 578 efc648d29dd0
child 805 96f51689cdeb