src/Pure/Syntax/token_trans.ML
changeset 6185 11bf7a8b6a02
parent 5989 9670dae0143d
child 6322 7047300264c9