src/ZF/Inductive.thy
changeset 24091 109f19a13872
parent 22814 4cd25f1706bb
child 24826 78e6a3cea367