src/ZF/Inductive.ML
changeset 4930 89271bc4e7ed
parent 4352 7ac9f3e8a97d
child 6053 8a1059aa01f0