src/Pure/Syntax/token_trans.ML
changeset 12618 43a97a2155d0
parent 11795 12a0fb3ac366
child 12785 27debaf2112d