src/Pure/Syntax/syntax.ML
changeset 63429 baedd4724f08
parent 63345 70b2313f9c52
child 64556 851ae0e7b09c
equal deleted inserted replaced
63428:005b490f0ce2 63429:baedd4724f08