src/ZF/ind_syntax.ML
changeset 1526 6be6ea6f8b5d
parent 1461 6bcb44e4d6e5
child 1738 a70a5bc5e315
equal deleted inserted replaced
1525:d127436567d0 1526:6be6ea6f8b5d