src/ZF/inductive.ML
changeset 5480 93c21fee39f8
parent 516 1957113f0d7d