src/ZF/ind_syntax.ML
changeset 16095 f6af6b265d20
parent 15570 8d8c70b41bab
child 16867 cf7d61d56acf
equal deleted inserted replaced
16094:a92ee2833938 16095:f6af6b265d20