src/ZF/Inductive.ML
changeset 4840 b8f2ec739530
parent 4352 7ac9f3e8a97d
child 6053 8a1059aa01f0