src/ZF/ind_syntax.ML
changeset 16709 a4679ac06502
parent 15570 8d8c70b41bab
child 16867 cf7d61d56acf
equal deleted inserted replaced
16708:479f7ac538b5 16709:a4679ac06502