src/ZF/inductive.thy
changeset 2334 00db792beb4e
parent 124 858ab9a9b047