src/ZF/Inductive.thy
changeset 592 9154d8410514
parent 578 efc648d29dd0
child 805 96f51689cdeb