src/ZF/inductive.thy
changeset 10155 6263a4a60e38
parent 124 858ab9a9b047