src/HOL/thy_syntax.ML
changeset 1669 e56cdf711729
parent 1668 8ead1fe65aad
child 1788 ca62fab4ce92
equal deleted inserted replaced
1668:8ead1fe65aad 1669:e56cdf711729