src/ZF/ind_syntax.ML
changeset 72755 8dffbe01a3e1
parent 69597 ff784d5a5bfb
child 74294 ee04dc00bf0a
equal deleted inserted replaced
72754:1456c5747416 72755:8dffbe01a3e1