src/HOL/thy_syntax.ML
changeset 6599 dc5bf3f40ad3
parent 6576 7e0b35bed503
child 6642 732af87c0650
equal deleted inserted replaced
6598:c1d7791f0314 6599:dc5bf3f40ad3