src/ZF/ind_syntax.ML
changeset 23015 e67f05cc0ac5
parent 22567 1565d476a9e2
child 23156 6ec9e29143e9