src/ZF/thy_syntax.ML
changeset 13218 3732064ccbd1
parent 12183 c10cea75dd56
child 14598 7009f59711e3
equal deleted inserted replaced
13217:bc5dc2392578 13218:3732064ccbd1